type name;
type ref;
const unique null : ref;
type real;
type elements;
type struct;
type exposeVersionType;
var $Heap : <x>[ref, name]x where IsHeap($Heap);
function IsHeap(h : <x>[ref, name]x) returns ($$unnamed~a : bool);
const $allocated : name;
const $elements : name;
const $inv : name;
const $localinv : name;
const $exposeVersion : name;
axiom (DeclType($exposeVersion) == System.Object);
const $sharingMode : name;
const $SharingMode_Unshared : name;
const $SharingMode_LockProtected : name;
const $ownerRef : name;
const $ownerFrame : name;
const $PeerGroupPlaceholder : name;
function ClassRepr(class : name) returns ($$unnamed~b : ref);
axiom (forall c0 : name, c1 : name :: {ClassRepr(c0), ClassRepr(c1)} ((c0 != c1) ==> (ClassRepr(c0) != ClassRepr(c1))));
axiom (forall T : name :: !($typeof(ClassRepr(T)) <: System.Object));
axiom (forall T : name :: (ClassRepr(T) != null));
axiom (forall T : name, h : <x>[ref, name]x :: {h[ClassRepr(T), $ownerFrame]} (IsHeap(h) ==> (h[ClassRepr(T), $ownerFrame] == $PeerGroupPlaceholder)));
function IsDirectlyModifiableField(f : name) returns ($$unnamed~c : bool);
axiom !IsDirectlyModifiableField($allocated);
axiom IsDirectlyModifiableField($elements);
axiom !IsDirectlyModifiableField($inv);
axiom !IsDirectlyModifiableField($localinv);
axiom !IsDirectlyModifiableField($ownerRef);
axiom !IsDirectlyModifiableField($ownerFrame);
axiom !IsDirectlyModifiableField($exposeVersion);
function IsStaticField(f : name) returns ($$unnamed~d : bool);
axiom !IsStaticField($allocated);
axiom !IsStaticField($elements);
axiom !IsStaticField($inv);
axiom !IsStaticField($localinv);
axiom !IsStaticField($exposeVersion);
function ValueArrayGet<any>($$unnamed~f : elements, $$unnamed~e : int) returns ($$unnamed~g : any);
function ValueArraySet<any>($$unnamed~j : elements, $$unnamed~i : int, $$unnamed~h : any) returns ($$unnamed~k : elements);
function RefArrayGet($$unnamed~m : elements, $$unnamed~l : int) returns ($$unnamed~n : ref);
function RefArraySet($$unnamed~q : elements, $$unnamed~p : int, $$unnamed~o : ref) returns ($$unnamed~r : elements);
axiom (forall<any> A : elements, i : int, x : any :: (ValueArrayGet(ValueArraySet(A, i, x), i) == x));
axiom (forall<any> A : elements, i : int, j : int, x : any :: ((i != j) ==> (ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(A, j))));
axiom (forall A : elements, i : int, x : ref :: (RefArrayGet(RefArraySet(A, i, x), i) == x));
axiom (forall A : elements, i : int, j : int, x : ref :: ((i != j) ==> (RefArrayGet(RefArraySet(A, i, x), j) == RefArrayGet(A, j))));
function ArrayIndex(arr : ref, dim : int, indexAtDim : int, remainingIndexContribution : int) returns ($$unnamed~s : int);
axiom (forall a : ref, d : int, x : int, y : int, x' : int, y' : int :: {ArrayIndex(a, d, x, y), ArrayIndex(a, d, x', y')} ((ArrayIndex(a, d, x, y) == ArrayIndex(a, d, x', y')) ==> ((x == x') && (y == y'))));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: RefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: RefArray(T, r))) ==> $Is(RefArrayGet(heap[a, $elements], i), T)));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: NonNullRefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: NonNullRefArray(T, r))) ==> $IsNotNull(RefArrayGet(heap[a, $elements], i), T)));
function $Rank($$unnamed~t : ref) returns ($$unnamed~u : int);
axiom (forall a : ref :: (1 <= $Rank(a)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: RefArray(T, r))} (((a != null) && ($typeof(a) <: RefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: NonNullRefArray(T, r))} (((a != null) && ($typeof(a) <: NonNullRefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: ValueArray(T, r))} (((a != null) && ($typeof(a) <: ValueArray(T, r))) ==> ($Rank(a) == r)));
function $Length($$unnamed~v : ref) returns ($$unnamed~w : int);
axiom (forall a : ref :: {$Length(a)} (0 <= $Length(a)));
function $DimLength($$unnamed~y : ref, $$unnamed~x : int) returns ($$unnamed~z : int);
axiom (forall a : ref, i : int :: (0 <= $DimLength(a, i)));
axiom (forall a : ref :: {$DimLength(a, 0)} (($Rank(a) == 1) ==> ($DimLength(a, 0) == $Length(a))));
function $LBound($$unnamed~ab : ref, $$unnamed~aa : int) returns ($$unnamed~ac : int);
function $UBound($$unnamed~ae : ref, $$unnamed~ad : int) returns ($$unnamed~af : int);
axiom (forall a : ref, i : int :: {$LBound(a, i)} ($LBound(a, i) == 0));
axiom (forall a : ref, i : int :: {$UBound(a, i)} ($UBound(a, i) == ($DimLength(a, i) - 1)));
const $ArrayCategoryValue : name;
const $ArrayCategoryRef : name;
const $ArrayCategoryNonNullRef : name;
function $ArrayCategory(arrayType : name) returns (arrayCategory : name);
axiom (forall T : name, ET : name, r : int :: {(T <: ValueArray(ET, r))} ((T <: ValueArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryValue)));
axiom (forall T : name, ET : name, r : int :: {(T <: RefArray(ET, r))} ((T <: RefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryRef)));
axiom (forall T : name, ET : name, r : int :: {(T <: NonNullRefArray(ET, r))} ((T <: NonNullRefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryNonNullRef)));
const System.Array : name;
axiom (System.Array <: System.Object);
function $ElementType($$unnamed~ag : name) returns ($$unnamed~ah : name);
function ValueArray(elementType : name, rank : int) returns ($$unnamed~ai : name);
axiom (forall T : name, r : int :: {ValueArray(T, r)} (ValueArray(T, r) <: System.Array));
function RefArray(elementType : name, rank : int) returns ($$unnamed~aj : name);
axiom (forall T : name, r : int :: {RefArray(T, r)} (RefArray(T, r) <: System.Array));
function NonNullRefArray(elementType : name, rank : int) returns ($$unnamed~ak : name);
axiom (forall T : name, r : int :: {NonNullRefArray(T, r)} (NonNullRefArray(T, r) <: System.Array));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (RefArray(U, r) <: RefArray(T, r))));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (NonNullRefArray(U, r) <: NonNullRefArray(T, r))));
axiom (forall A : name, r : int :: ($ElementType(ValueArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(RefArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(NonNullRefArray(A, r)) == A));
axiom (forall A : name, r : int, T : name :: {(T <: RefArray(A, r))} ((T <: RefArray(A, r)) ==> ((T == RefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: NonNullRefArray(A, r))} ((T <: NonNullRefArray(A, r)) ==> ((T == NonNullRefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: ValueArray(A, r))} ((T <: ValueArray(A, r)) ==> (T == ValueArray(A, r))));
axiom (forall A : name, r : int, T : name :: ((RefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == RefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((NonNullRefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == NonNullRefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((ValueArray(A, r) <: T) ==> ((System.Array <: T) || (T == ValueArray(A, r)))));
function $ArrayPtr(elementType : name) returns ($$unnamed~al : name);
function $StructGet<any>($$unnamed~an : struct, $$unnamed~am : name) returns ($$unnamed~ao : any);
function $StructSet<any>($$unnamed~ar : struct, $$unnamed~aq : name, $$unnamed~ap : any) returns ($$unnamed~as : struct);
axiom (forall<any> s : struct, f : name, x : any :: ($StructGet($StructSet(s, f, x), f) == x));
axiom (forall<any> s : struct, f : name, f' : name, x : any :: ((f != f') ==> ($StructGet($StructSet(s, f, x), f') == $StructGet(s, f'))));
function ZeroInit(s : struct, typ : name) returns ($$unnamed~at : bool);
function $typeof($$unnamed~au : ref) returns ($$unnamed~av : name);
function $BaseClass(sub : name) returns (base : name);
function AsDirectSubClass(sub : name, base : name) returns (sub' : name);
function OneClassDown(sub : name, base : name) returns (directSub : name);
axiom (forall A : name, B : name, C : name :: {(C <: AsDirectSubClass(B, A))} ((C <: AsDirectSubClass(B, A)) ==> (OneClassDown(C, A) == B)));
function $IsValueType($$unnamed~aw : name) returns ($$unnamed~ax : bool);
axiom (forall T : name :: ($IsValueType(T) ==> ((forall U : name :: ((T <: U) ==> (T == U))) && (forall U : name :: ((U <: T) ==> (T == U))))));
const System.Object : name;
function $IsTokenForType($$unnamed~az : struct, $$unnamed~ay : name) returns ($$unnamed~ba : bool);
function TypeObject($$unnamed~bb : name) returns ($$unnamed~bc : ref);
const System.Type : name;
axiom (System.Type <: System.Object);
axiom (forall T : name :: {TypeObject(T)} $IsNotNull(TypeObject(T), System.Type));
function TypeName($$unnamed~bd : ref) returns ($$unnamed~be : name);
axiom (forall T : name :: {TypeObject(T)} (TypeName(TypeObject(T)) == T));
function $Is($$unnamed~bg : ref, $$unnamed~bf : name) returns ($$unnamed~bh : bool);
axiom (forall o : ref, T : name :: {$Is(o, T)} ($Is(o, T) <==> ((o == null) || ($typeof(o) <: T))));
function $IsNotNull($$unnamed~bj : ref, $$unnamed~bi : name) returns ($$unnamed~bk : bool);
axiom (forall o : ref, T : name :: {$IsNotNull(o, T)} ($IsNotNull(o, T) <==> ((o != null) && $Is(o, T))));
function $As($$unnamed~bm : ref, $$unnamed~bl : name) returns ($$unnamed~bn : ref);
axiom (forall o : ref, T : name :: ($Is(o, T) ==> ($As(o, T) == o)));
axiom (forall o : ref, T : name :: (!$Is(o, T) ==> ($As(o, T) == null)));
axiom (forall h : <x>[ref, name]x, o : ref :: {($typeof(o) <: System.Array), h[o, $inv]} (((IsHeap(h) && (o != null)) && ($typeof(o) <: System.Array)) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
function IsAllocated<any>(h : <x>[ref, name]x, o : any) returns ($$unnamed~bo : bool);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {IsAllocated(h, h[o, f])} ((IsHeap(h) && h[o, $allocated]) ==> IsAllocated(h, h[o, f])));
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[h[o, f], $allocated]} ((IsHeap(h) && h[o, $allocated]) ==> h[h[o, f], $allocated]));
axiom (forall h : <x>[ref, name]x, s : struct, f : name :: {IsAllocated(h, $StructGet(s, f))} (IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, RefArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, ValueArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, ValueArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, o : ref :: {h[o, $allocated]} (IsAllocated(h, o) ==> h[o, $allocated]));
axiom (forall h : <x>[ref, name]x, c : name :: {h[ClassRepr(c), $allocated]} (IsHeap(h) ==> h[ClassRepr(c), $allocated]));
const $BeingConstructed : ref;
const $NonNullFieldsAreInitialized : name;
function DeclType(field : name) returns (class : name);
function AsNonNullRefField(field : name, T : name) returns (f : name);
function AsRefField(field : name, T : name) returns (f : name);
function AsRangeField(field : name, T : name) returns (f : name);
axiom (forall f : name, T : name :: {AsNonNullRefField(f, T)} ((AsNonNullRefField(f, T) == f) ==> (AsRefField(f, T) == f)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRefField(f, T)]} (IsHeap(h) ==> $Is(h[o, AsRefField(f, T)], T)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsNonNullRefField(f, T)]} (((IsHeap(h) && (o != null)) && ((o != $BeingConstructed) || (h[$BeingConstructed, $NonNullFieldsAreInitialized] == true))) ==> (h[o, AsNonNullRefField(f, T)] != null)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRangeField(f, T)]} (IsHeap(h) ==> InRange(h[o, AsRangeField(f, T)], T)));
function $IsMemberlessType($$unnamed~bp : name) returns ($$unnamed~bq : bool);
axiom (forall o : ref :: {$IsMemberlessType($typeof(o))} !$IsMemberlessType($typeof(o)));
function $IsImmutable(T : name) returns ($$unnamed~br : bool);
axiom !$IsImmutable(System.Object);
function $AsImmutable(T : name) returns (theType : name);
function $AsMutable(T : name) returns (theType : name);
axiom (forall T : name, U : name :: {(U <: $AsImmutable(T))} ((U <: $AsImmutable(T)) ==> ($IsImmutable(U) && ($AsImmutable(U) == U))));
axiom (forall T : name, U : name :: {(U <: $AsMutable(T))} ((U <: $AsMutable(T)) ==> (!$IsImmutable(U) && ($AsMutable(U) == U))));
function AsOwner(string : ref, owner : ref) returns (theString : ref);
axiom (forall o : ref, T : name :: {($typeof(o) <: $AsImmutable(T))} ((((o != null) && (o != $BeingConstructed)) && ($typeof(o) <: $AsImmutable(T))) ==> (forall h : <x>[ref, name]x :: {IsHeap(h)} (IsHeap(h) ==> (((((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o))) && (h[o, $ownerFrame] == $PeerGroupPlaceholder)) && (AsOwner(o, h[o, $ownerRef]) == o)) && (forall t : ref :: {AsOwner(o, h[t, $ownerRef])} ((AsOwner(o, h[t, $ownerRef]) == o) ==> ((t == o) || (h[t, $ownerFrame] != $PeerGroupPlaceholder)))))))));
const System.String : name;
function $StringLength($$unnamed~bs : ref) returns ($$unnamed~bt : int);
axiom (forall s : ref :: {$StringLength(s)} (0 <= $StringLength(s)));
function AsRepField(f : name, declaringType : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRepField(f, T)]} ((IsHeap(h) && (h[o, AsRepField(f, T)] != null)) ==> ((h[h[o, AsRepField(f, T)], $ownerRef] == o) && (h[h[o, AsRepField(f, T)], $ownerFrame] == T))));
function AsPeerField(f : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[o, AsPeerField(f)]} ((IsHeap(h) && (h[o, AsPeerField(f)] != null)) ==> ((h[h[o, AsPeerField(f)], $ownerRef] == h[o, $ownerRef]) && (h[h[o, AsPeerField(f)], $ownerFrame] == h[o, $ownerFrame]))));
axiom (forall h : <x>[ref, name]x, o : ref :: {(h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])} ((((IsHeap(h) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
procedure $SetOwner(o : ref, ow : ref, fr : name);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[o, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[o, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[o, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[o, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == ow) && ($Heap[p, $ownerFrame] == fr))));
  

procedure $UpdateOwnersForRep(o : ref, T : name, e : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[e, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[e, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((e == null) ==> ($Heap == old($Heap)));
  ensures ((e != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[e, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[e, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == o) && ($Heap[p, $ownerFrame] == T)))));
  

procedure $UpdateOwnersForPeer(c : ref, d : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} ((((F != $ownerRef) && (F != $ownerFrame)) || old(((($Heap[p, $ownerRef] != $Heap[c, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[c, $ownerFrame])) && (($Heap[p, $ownerRef] != $Heap[d, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[d, $ownerFrame]))))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((d == null) ==> ($Heap == old($Heap)));
  ensures ((d != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} (((old(($Heap[p, $ownerRef] == $Heap[c, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[c, $ownerFrame]))) || (old(($Heap[p, $ownerRef] == $Heap[d, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[d, $ownerFrame])))) ==> ((((old($Heap)[d, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[c, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[c, $ownerFrame])) || (((old($Heap)[d, $ownerFrame] != $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[d, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[d, $ownerFrame]))))));
  

const $FirstConsistentOwner : name;
function $AsPureObject($$unnamed~bu : ref) returns ($$unnamed~bv : ref);
function ##FieldDependsOnFCO<any>(o : ref, f : name, ev : exposeVersionType) returns (value : any);
axiom (forall o : ref, f : name, h : <x>[ref, name]x :: {h[$AsPureObject(o), f]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (h[o, f] == ##FieldDependsOnFCO(o, f, h[h[o, $FirstConsistentOwner], $exposeVersion]))));
axiom (forall o : ref, h : <x>[ref, name]x :: {h[o, $FirstConsistentOwner]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (((h[o, $FirstConsistentOwner] != null) && (h[h[o, $FirstConsistentOwner], $allocated] == true)) && (((h[h[o, $FirstConsistentOwner], $ownerFrame] == $PeerGroupPlaceholder) || !(h[h[h[o, $FirstConsistentOwner], $ownerRef], $inv] <: h[h[o, $FirstConsistentOwner], $ownerFrame])) || (h[h[h[o, $FirstConsistentOwner], $ownerRef], $localinv] == $BaseClass(h[h[o, $FirstConsistentOwner], $ownerFrame]))))));
function Box<any>($$unnamed~bx : any, $$unnamed~bw : ref) returns ($$unnamed~by : ref);
function Unbox<any>($$unnamed~bz : ref) returns ($$unnamed~ca : any);
axiom (forall<any> x : any, p : ref :: {Unbox(Box(x, p))} (Unbox(Box(x, p)) == x));
function UnboxedType($$unnamed~cb : ref) returns ($$unnamed~cc : name);
axiom (forall p : ref :: {$IsValueType(UnboxedType(p))} ($IsValueType(UnboxedType(p)) ==> (forall<any> heap : <x>[ref, name]x, x : any :: {heap[Box(x, p), $inv]} (IsHeap(heap) ==> ((heap[Box(x, p), $inv] == $typeof(Box(x, p))) && (heap[Box(x, p), $localinv] == $typeof(Box(x, p))))))));
axiom (forall<any> x : any, p : ref :: {(UnboxedType(Box(x, p)) <: System.Object)} (((UnboxedType(Box(x, p)) <: System.Object) && (Box(x, p) == p)) ==> (x == p)));
function BoxTester(p : ref, typ : name) returns ($$unnamed~cd : ref);
axiom (forall p : ref, typ : name :: {BoxTester(p, typ)} ((UnboxedType(p) == typ) <==> (BoxTester(p, typ) != null)));
const System.SByte : name;
axiom $IsValueType(System.SByte);
const System.Byte : name;
axiom $IsValueType(System.Byte);
const System.Int16 : name;
axiom $IsValueType(System.Int16);
const System.UInt16 : name;
axiom $IsValueType(System.UInt16);
const System.Int32 : name;
axiom $IsValueType(System.Int32);
const System.UInt32 : name;
axiom $IsValueType(System.UInt32);
const System.Int64 : name;
axiom $IsValueType(System.Int64);
const System.UInt64 : name;
axiom $IsValueType(System.UInt64);
const System.Char : name;
axiom $IsValueType(System.Char);
const int#m2147483648 : int;
const int#2147483647 : int;
const int#4294967295 : int;
const int#m9223372036854775808 : int;
const int#9223372036854775807 : int;
const int#18446744073709551615 : int;
axiom (int#m9223372036854775808 < int#m2147483648);
axiom (int#m2147483648 < (0 - 100000));
axiom (100000 < int#2147483647);
axiom (int#2147483647 < int#4294967295);
axiom (int#4294967295 < int#9223372036854775807);
axiom (int#9223372036854775807 < int#18446744073709551615);
function InRange(i : int, T : name) returns ($$unnamed~ce : bool);
axiom (forall i : int :: (InRange(i, System.SByte) <==> (((0 - 128) <= i) && (i < 128))));
axiom (forall i : int :: (InRange(i, System.Byte) <==> ((0 <= i) && (i < 256))));
axiom (forall i : int :: (InRange(i, System.Int16) <==> (((0 - 32768) <= i) && (i < 32768))));
axiom (forall i : int :: (InRange(i, System.UInt16) <==> ((0 <= i) && (i < 65536))));
axiom (forall i : int :: (InRange(i, System.Int32) <==> ((int#m2147483648 <= i) && (i <= int#2147483647))));
axiom (forall i : int :: (InRange(i, System.UInt32) <==> ((0 <= i) && (i <= int#4294967295))));
axiom (forall i : int :: (InRange(i, System.Int64) <==> ((int#m9223372036854775808 <= i) && (i <= int#9223372036854775807))));
axiom (forall i : int :: (InRange(i, System.UInt64) <==> ((0 <= i) && (i <= int#18446744073709551615))));
axiom (forall i : int :: (InRange(i, System.Char) <==> ((0 <= i) && (i < 65536))));
function $IntToInt(val : int, fromType : name, toType : name) returns ($$unnamed~cf : int);
function $IntToReal($$unnamed~cg : int, fromType : name, toType : name) returns ($$unnamed~ch : real);
function $RealToInt($$unnamed~ci : real, fromType : name, toType : name) returns ($$unnamed~cj : int);
function $RealToReal(val : real, fromType : name, toType : name) returns ($$unnamed~ck : real);
function $SizeIs($$unnamed~cm : name, $$unnamed~cl : int) returns ($$unnamed~cn : bool);
function $IfThenElse<any>($$unnamed~cq : bool, $$unnamed~cp : any, $$unnamed~co : any) returns ($$unnamed~cr : any);
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (b ==> ($IfThenElse(b, x, y) == x)));
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (!b ==> ($IfThenElse(b, x, y) == y)));
function #neg($$unnamed~cs : int) returns ($$unnamed~ct : int);
function #and($$unnamed~cv : int, $$unnamed~cu : int) returns ($$unnamed~cw : int);
function #or($$unnamed~cy : int, $$unnamed~cx : int) returns ($$unnamed~cz : int);
function #xor($$unnamed~db : int, $$unnamed~da : int) returns ($$unnamed~dc : int);
function #shl($$unnamed~de : int, $$unnamed~dd : int) returns ($$unnamed~df : int);
function #shr($$unnamed~dh : int, $$unnamed~dg : int) returns ($$unnamed~di : int);
function #rneg($$unnamed~dj : real) returns ($$unnamed~dk : real);
function #radd($$unnamed~dm : real, $$unnamed~dl : real) returns ($$unnamed~dn : real);
function #rsub($$unnamed~dp : real, $$unnamed~do : real) returns ($$unnamed~dq : real);
function #rmul($$unnamed~ds : real, $$unnamed~dr : real) returns ($$unnamed~dt : real);
function #rdiv($$unnamed~dv : real, $$unnamed~du : real) returns ($$unnamed~dw : real);
function #rmod($$unnamed~dy : real, $$unnamed~dx : real) returns ($$unnamed~dz : real);
function #rLess($$unnamed~eb : real, $$unnamed~ea : real) returns ($$unnamed~ec : bool);
function #rAtmost($$unnamed~ee : real, $$unnamed~ed : real) returns ($$unnamed~ef : bool);
function #rEq($$unnamed~eh : real, $$unnamed~eg : real) returns ($$unnamed~ei : bool);
function #rNeq($$unnamed~ek : real, $$unnamed~ej : real) returns ($$unnamed~el : bool);
function #rAtleast($$unnamed~en : real, $$unnamed~em : real) returns ($$unnamed~eo : bool);
function #rGreater($$unnamed~eq : real, $$unnamed~ep : real) returns ($$unnamed~er : bool);
axiom (forall x : int, y : int :: {(x % y)} {(x / y)} ((x % y) == (x - ((x / y) * y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (0 < y)) ==> ((0 <= (x % y)) && ((x % y) < y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (y < 0)) ==> ((0 <= (x % y)) && ((x % y) < (0 - y)))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (0 < y)) ==> (((0 - y) < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (y < 0)) ==> ((y < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {((x + y) % y)} (((0 <= x) && (0 <= y)) ==> (((x + y) % y) == (x % y))));
axiom (forall x : int, y : int :: {((y + x) % y)} (((0 <= x) && (0 <= y)) ==> (((y + x) % y) == (x % y))));
axiom (forall x : int, y : int :: {((x - y) % y)} (((0 <= (x - y)) && (0 <= y)) ==> (((x - y) % y) == (x % y))));
axiom (forall a : int, b : int, d : int :: {(a % d), (b % d)} ((((2 <= d) && ((a % d) == (b % d))) && (a < b)) ==> ((a + d) <= b)));
axiom (forall x : int, y : int :: {#and(x, y)} (((0 <= x) || (0 <= y)) ==> (0 <= #and(x, y))));
axiom (forall x : int, y : int :: {#or(x, y)} (((0 <= x) && (0 <= y)) ==> ((0 <= #or(x, y)) && (#or(x, y) <= (x + y)))));
axiom (forall i : int :: {#shl(i, 0)} (#shl(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shl(i, (j + 1)) == (#shl(i, j) * 2))));
axiom (forall i : int :: {#shr(i, 0)} (#shr(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shr(i, (j + 1)) == (#shr(i, j) / 2))));
function #System.String.IsInterned$System.String$notnull($$unnamed~es : ref) returns ($$unnamed~et : ref);
function #System.String.Equals$System.String($$unnamed~ev : ref, $$unnamed~eu : ref) returns ($$unnamed~ew : bool);
function #System.String.Equals$System.String$System.String($$unnamed~ey : ref, $$unnamed~ex : ref) returns ($$unnamed~ez : bool);
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String(a, b)} (#System.String.Equals$System.String(a, b) == #System.String.Equals$System.String$System.String(a, b)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} (#System.String.Equals$System.String$System.String(a, b) == #System.String.Equals$System.String$System.String(b, a)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} ((((a != null) && (b != null)) && #System.String.Equals$System.String$System.String(a, b)) ==> (#System.String.IsInterned$System.String$notnull(a) == #System.String.IsInterned$System.String$notnull(b))));
const $UnknownRef : ref;
const BasicMethodology.ec : name;
const Component.y : name;
const CS.f : name;
const BasicMethodology.c : name;
const BasicMethodology.x : name;
const System.IComparable`1...System.String : name;
const System.IEquatable`1...System.String : name;
const System.Boolean : name;
const System.Runtime.InteropServices._Exception : name;
const ExtensibleComponent : name;
const Component : name;
const C : name;
const BasicMethodology : name;
const System.Reflection.IReflect : name;
const System.Runtime.InteropServices._MemberInfo : name;
const Microsoft.Contracts.ObjectInvariantException : name;
const System.Reflection.MemberInfo : name;
const Microsoft.Contracts.GuardException : name;
const SubClass : name;
const System.IConvertible : name;
const System.Runtime.Serialization.ISerializable : name;
const System.Runtime.InteropServices._Type : name;
const CS : name;
const System.IComparable : name;
const System.Exception : name;
const System.Reflection.ICustomAttributeProvider : name;
const Microsoft.Contracts.ICheckedException : name;
const System.Collections.IEnumerable : name;
const System.Collections.Generic.IEnumerable`1...System.Char : name;
const System.ICloneable : name;
axiom !IsStaticField(BasicMethodology.x);
axiom IsDirectlyModifiableField(BasicMethodology.x);
axiom (DeclType(BasicMethodology.x) == BasicMethodology);
axiom (AsRangeField(BasicMethodology.x, System.Int32) == BasicMethodology.x);
axiom !IsStaticField(Component.y);
axiom IsDirectlyModifiableField(Component.y);
axiom (DeclType(Component.y) == Component);
axiom (AsRangeField(Component.y, System.Int32) == Component.y);
axiom !IsStaticField(BasicMethodology.c);
axiom IsDirectlyModifiableField(BasicMethodology.c);
axiom (AsRepField(BasicMethodology.c, BasicMethodology) == BasicMethodology.c);
axiom (DeclType(BasicMethodology.c) == BasicMethodology);
axiom (AsNonNullRefField(BasicMethodology.c, Component) == BasicMethodology.c);
axiom !IsStaticField(BasicMethodology.ec);
axiom IsDirectlyModifiableField(BasicMethodology.ec);
axiom (AsRepField(BasicMethodology.ec, BasicMethodology) == BasicMethodology.ec);
axiom (DeclType(BasicMethodology.ec) == BasicMethodology);
axiom (AsNonNullRefField(BasicMethodology.ec, ExtensibleComponent) == BasicMethodology.ec);
axiom !IsStaticField(CS.f);
axiom IsDirectlyModifiableField(CS.f);
axiom (DeclType(CS.f) == CS);
axiom (AsRangeField(CS.f, System.Int32) == CS.f);
axiom (BasicMethodology <: BasicMethodology);
axiom ($BaseClass(BasicMethodology) == System.Object);
axiom ((BasicMethodology <: $BaseClass(BasicMethodology)) && (AsDirectSubClass(BasicMethodology, $BaseClass(BasicMethodology)) == BasicMethodology));
axiom (!$IsImmutable(BasicMethodology) && ($AsMutable(BasicMethodology) == BasicMethodology));
axiom (Component <: Component);
axiom ($BaseClass(Component) == System.Object);
axiom ((Component <: $BaseClass(Component)) && (AsDirectSubClass(Component, $BaseClass(Component)) == Component));
axiom (!$IsImmutable(Component) && ($AsMutable(Component) == Component));
axiom (forall $U : name :: {($U <: Component)} (($U <: Component) ==> ($U == Component)));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: Component)} (((IsHeap($h) && ($h[$oi, $inv] <: Component)) && ($h[$oi, $localinv] != System.Object)) ==> ($h[$oi, Component.y] <= 80)));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: BasicMethodology)} (((IsHeap($h) && ($h[$oi, $inv] <: BasicMethodology)) && ($h[$oi, $localinv] != System.Object)) ==> ((10 <= $h[$oi, BasicMethodology.x]) && ($h[$oi, BasicMethodology.x] <= $h[$h[$oi, BasicMethodology.c], Component.y]))));
axiom (forall $U : name :: {($U <: System.Boolean)} (($U <: System.Boolean) ==> ($U == System.Boolean)));
procedure BasicMethodology.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation BasicMethodology.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var return.value : bool where true;
  var stack50000o : ref;
  var stack0o : ref;
  var stack1o : ref;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, BasicMethodology); goto $$entry~b;
  $$entry~b: assume ($Heap[this, $allocated] == true); goto $$entry~a;
  $$entry~a: throwException := throwException$in; goto block6069;
  block6069: goto block6086;
  block6086: stack0i := 10; goto $$block6086~b;
  $$block6086~b: assert (this != null); goto $$block6086~a;
  $$block6086~a: stack1i := $Heap[this, BasicMethodology.x]; goto true6086to6205, false6086to6103;
  true6086to6205: assume (stack0i <= stack1i); goto block6205;
  false6086to6103: assume (stack0i > stack1i); goto block6103;
  block6205: goto block6222;
  block6103: stack0b := throwException; goto true6103to6154, false6103to6120;
  true6103to6154: assume !stack0b; goto block6154;
  false6103to6120: assume stack0b; goto block6120;
  block6154: return.value := false; goto block6409;
  block6120: assume false; goto $$block6120~i;
  $$block6120~i: havoc stack50000o; goto $$block6120~h;
  $$block6120~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block6120~g;
  $$block6120~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block6120~f;
  $$block6120~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block6120~e;
  $$block6120~e: assert (stack50000o != null); goto $$block6120~d;
  $$block6120~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block6120~c;
  $$block6120~c: stack0o := stack50000o; goto $$block6120~b;
  $$block6120~b: assert (stack0o != null); goto $$block6120~a;
  $$block6120~a: assume false; return;
  block6222: goto block6239;
  block6409: goto block6426;
  block6239: assert (this != null); goto $$block6239~e;
  $$block6239~e: stack0i := $Heap[this, BasicMethodology.x]; goto $$block6239~d;
  $$block6239~d: assert (this != null); goto $$block6239~c;
  $$block6239~c: stack1o := $Heap[this, BasicMethodology.c]; goto $$block6239~b;
  $$block6239~b: assert (stack1o != null); goto $$block6239~a;
  $$block6239~a: stack1i := $Heap[stack1o, Component.y]; goto true6239to6358, false6239to6256;
  true6239to6358: assume (stack0i <= stack1i); goto block6358;
  false6239to6256: assume (stack0i > stack1i); goto block6256;
  block6358: goto block6375;
  block6256: stack0b := throwException; goto true6256to6307, false6256to6273;
  block6426: SS$Display.Return.Local := return.value; goto $$block6426~b;
  $$block6426~b: stack0b := return.value; goto $$block6426~a;
  $$block6426~a: $result := stack0b; return;
  true6256to6307: assume !stack0b; goto block6307;
  false6256to6273: assume stack0b; goto block6273;
  block6307: return.value := false; goto block6409;
  block6273: assume false; goto $$block6273~i;
  $$block6273~i: havoc stack50000o; goto $$block6273~h;
  $$block6273~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block6273~g;
  $$block6273~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block6273~f;
  $$block6273~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block6273~e;
  $$block6273~e: assert (stack50000o != null); goto $$block6273~d;
  $$block6273~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block6273~c;
  $$block6273~c: stack0o := stack50000o; goto $$block6273~b;
  $$block6273~b: assert (stack0o != null); goto $$block6273~a;
  $$block6273~a: assume false; return;
  block6375: goto block6392;
  block6392: return.value := true; goto block6409;
  
}

axiom (Microsoft.Contracts.ObjectInvariantException <: Microsoft.Contracts.ObjectInvariantException);
axiom (Microsoft.Contracts.GuardException <: Microsoft.Contracts.GuardException);
axiom (System.Exception <: System.Exception);
axiom ($BaseClass(System.Exception) == System.Object);
axiom ((System.Exception <: $BaseClass(System.Exception)) && (AsDirectSubClass(System.Exception, $BaseClass(System.Exception)) == System.Exception));
axiom (!$IsImmutable(System.Exception) && ($AsMutable(System.Exception) == System.Exception));
axiom (System.Runtime.Serialization.ISerializable <: System.Object);
axiom $IsMemberlessType(System.Runtime.Serialization.ISerializable);
axiom (System.Exception <: System.Runtime.Serialization.ISerializable);
axiom (System.Runtime.InteropServices._Exception <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Exception);
axiom (System.Exception <: System.Runtime.InteropServices._Exception);
axiom ($BaseClass(Microsoft.Contracts.GuardException) == System.Exception);
axiom ((Microsoft.Contracts.GuardException <: $BaseClass(Microsoft.Contracts.GuardException)) && (AsDirectSubClass(Microsoft.Contracts.GuardException, $BaseClass(Microsoft.Contracts.GuardException)) == Microsoft.Contracts.GuardException));
axiom (!$IsImmutable(Microsoft.Contracts.GuardException) && ($AsMutable(Microsoft.Contracts.GuardException) == Microsoft.Contracts.GuardException));
axiom ($BaseClass(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.GuardException);
axiom ((Microsoft.Contracts.ObjectInvariantException <: $BaseClass(Microsoft.Contracts.ObjectInvariantException)) && (AsDirectSubClass(Microsoft.Contracts.ObjectInvariantException, $BaseClass(Microsoft.Contracts.ObjectInvariantException)) == Microsoft.Contracts.ObjectInvariantException));
axiom (!$IsImmutable(Microsoft.Contracts.ObjectInvariantException) && ($AsMutable(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.ObjectInvariantException));
procedure Microsoft.Contracts.ObjectInvariantException..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Microsoft.Contracts.ObjectInvariantException)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Microsoft.Contracts.ObjectInvariantException <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure BasicMethodology.P(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == BasicMethodology)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation BasicMethodology.P(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local8976 : ref where $Is(local8976, System.Exception);
  var stack0i : int;
  var stack1o : ref;
  var stack1i : int;
  var stack0b : bool;
  var local9010 : int where InRange(local9010, System.Int32);
  var local8993 : int where InRange(local8993, System.Int32);
  var stack0o : ref;
  entry: assume $IsNotNull(this, BasicMethodology); goto $$entry~c;
  $$entry~c: assume ($Heap[this, $allocated] == true); goto block7990;
  block7990: goto block8245;
  block8245: goto block8262;
  block8262: temp0 := this; goto $$block8262~g;
  $$block8262~g: assert (temp0 != null); goto $$block8262~f;
  $$block8262~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == BasicMethodology)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block8262~e;
  $$block8262~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block8262~d;
  $$block8262~d: havoc temp1; goto $$block8262~c;
  $$block8262~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block8262~b;
  $$block8262~b: assume IsHeap($Heap); goto $$block8262~a;
  $$block8262~a: local8976 := null; goto block8279;
  block8279: assert (this != null); goto $$block8279~e;
  $$block8279~e: stack0i := $Heap[this, BasicMethodology.x]; goto $$block8279~d;
  $$block8279~d: assert (this != null); goto $$block8279~c;
  $$block8279~c: stack1o := $Heap[this, BasicMethodology.c]; goto $$block8279~b;
  $$block8279~b: assert (stack1o != null); goto $$block8279~a;
  $$block8279~a: stack1i := $Heap[stack1o, Component.y]; goto true8279to8347, false8279to8296;
  true8279to8347: assume (stack0i >= stack1i); goto block8347;
  false8279to8296: assume (stack0i < stack1i); goto block8296;
  block8347: stack0i := 10; goto $$block8347~b;
  $$block8347~b: assert (this != null); goto $$block8347~a;
  $$block8347~a: stack1i := $Heap[this, BasicMethodology.x]; goto true8347to8398, false8347to8364;
  block8296: assert (this != null); goto $$block8296~h;
  $$block8296~h: local9010 := $Heap[this, BasicMethodology.x]; goto $$block8296~g;
  $$block8296~g: stack0i := 1; goto $$block8296~f;
  $$block8296~f: stack0i := (local9010 + stack0i); goto $$block8296~e;
  $$block8296~e: assert (this != null); goto $$block8296~d;
  $$block8296~d: assert !($Heap[this, $inv] <: BasicMethodology); goto $$block8296~c;
  $$block8296~c: $Heap := $Heap[this, BasicMethodology.x := stack0i]; goto $$block8296~b;
  $$block8296~b: assume IsHeap($Heap); goto $$block8296~a;
  $$block8296~a: stack0i := local9010; goto block8313;
  true8347to8398: assume (stack0i >= stack1i); goto block8398;
  false8347to8364: assume (stack0i < stack1i); goto block8364;
  block8398: goto block8415;
  block8364: assert (this != null); goto $$block8364~h;
  $$block8364~h: local8993 := $Heap[this, BasicMethodology.x]; goto $$block8364~g;
  $$block8364~g: stack0i := 1; goto $$block8364~f;
  $$block8364~f: stack0i := (local8993 - stack0i); goto $$block8364~e;
  $$block8364~e: assert (this != null); goto $$block8364~d;
  $$block8364~d: assert !($Heap[this, $inv] <: BasicMethodology); goto $$block8364~c;
  $$block8364~c: $Heap := $Heap[this, BasicMethodology.x := stack0i]; goto $$block8364~b;
  $$block8364~b: assume IsHeap($Heap); goto $$block8364~a;
  $$block8364~a: stack0i := local8993; goto block8381;
  block8313: goto block8330;
  block8415: goto block8432;
  block8381: goto block8398;
  block8330: goto block8432;
  block8432: goto block8449;
  block8449: goto block8619;
  block8619: stack0o := null; goto true8619to8721, false8619to8636;
  true8619to8721: assume (local8976 == stack0o); goto block8721;
  false8619to8636: assume (local8976 != stack0o); goto block8636;
  block8721: goto block8738;
  block8636: goto true8636to8721, false8636to8653;
  true8636to8721: assume ($As(local8976, Microsoft.Contracts.ICheckedException) != null); goto block8721;
  false8636to8653: assume ($As(local8976, Microsoft.Contracts.ICheckedException) == null); goto block8653;
  block8653: goto block8670;
  block8738: assert (temp0 != null); goto $$block8738~f;
  $$block8738~f: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block8738~e;
  $$block8738~e: assert (10 <= $Heap[temp0, BasicMethodology.x]); goto $$block8738~d;
  $$block8738~d: assert ($Heap[temp0, BasicMethodology.x] <= $Heap[$Heap[temp0, BasicMethodology.c], Component.y]); goto $$block8738~c;
  $$block8738~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == BasicMethodology)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block8738~b;
  $$block8738~b: $Heap := $Heap[temp0, $inv := BasicMethodology]; goto $$block8738~a;
  $$block8738~a: assume IsHeap($Heap); goto block8670;
  block8670: goto block8687;
  block8687: goto block8704;
  block8704: goto block8568;
  block8568: goto block8585;
  block8585: goto block8602;
  block8602: return;
  
}

axiom (Microsoft.Contracts.ICheckedException <: System.Object);
axiom $IsMemberlessType(Microsoft.Contracts.ICheckedException);
procedure BasicMethodology.PeekBelow(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == BasicMethodology)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation BasicMethodology.PeekBelow(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local11254 : ref where $Is(local11254, System.Exception);
  var stack0o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, BasicMethodology); goto $$entry~d;
  $$entry~d: assume ($Heap[this, $allocated] == true); goto block10064;
  block10064: goto block10319;
  block10319: goto block10336;
  block10336: temp0 := this; goto $$block10336~g;
  $$block10336~g: assert (temp0 != null); goto $$block10336~f;
  $$block10336~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == BasicMethodology)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block10336~e;
  $$block10336~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block10336~d;
  $$block10336~d: havoc temp1; goto $$block10336~c;
  $$block10336~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block10336~b;
  $$block10336~b: assume IsHeap($Heap); goto $$block10336~a;
  $$block10336~a: local11254 := null; goto block10353;
  block10353: assert ((((($Heap[$Heap[this, BasicMethodology.ec], $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[$Heap[this, BasicMethodology.ec], $ownerRef], $inv] <: $Heap[$Heap[this, BasicMethodology.ec], $ownerFrame])) || ($Heap[$Heap[$Heap[this, BasicMethodology.ec], $ownerRef], $localinv] == $BaseClass($Heap[$Heap[this, BasicMethodology.ec], $ownerFrame]))) && ($Heap[$Heap[this, BasicMethodology.ec], $inv] == $typeof($Heap[this, BasicMethodology.ec]))) && ($Heap[$Heap[this, BasicMethodology.ec], $localinv] == $typeof($Heap[this, BasicMethodology.ec]))); goto block10506;
  block10506: goto block10523;
  block10523: assert ((((($Heap[$Heap[this, BasicMethodology.c], $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[$Heap[this, BasicMethodology.c], $ownerRef], $inv] <: $Heap[$Heap[this, BasicMethodology.c], $ownerFrame])) || ($Heap[$Heap[$Heap[this, BasicMethodology.c], $ownerRef], $localinv] == $BaseClass($Heap[$Heap[this, BasicMethodology.c], $ownerFrame]))) && ($Heap[$Heap[this, BasicMethodology.c], $inv] == Component)) && ($Heap[$Heap[this, BasicMethodology.c], $localinv] == $typeof($Heap[this, BasicMethodology.c]))); goto block10676;
  block10676: goto block10693;
  block10693: goto block10863;
  block10863: stack0o := null; goto true10863to10965, false10863to10880;
  true10863to10965: assume (local11254 == stack0o); goto block10965;
  false10863to10880: assume (local11254 != stack0o); goto block10880;
  block10965: goto block10982;
  block10880: goto true10880to10965, false10880to10897;
  true10880to10965: assume ($As(local11254, Microsoft.Contracts.ICheckedException) != null); goto block10965;
  false10880to10897: assume ($As(local11254, Microsoft.Contracts.ICheckedException) == null); goto block10897;
  block10897: goto block10914;
  block10982: assert (temp0 != null); goto $$block10982~f;
  $$block10982~f: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block10982~e;
  $$block10982~e: assert (10 <= $Heap[temp0, BasicMethodology.x]); goto $$block10982~d;
  $$block10982~d: assert ($Heap[temp0, BasicMethodology.x] <= $Heap[$Heap[temp0, BasicMethodology.c], Component.y]); goto $$block10982~c;
  $$block10982~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == BasicMethodology)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block10982~b;
  $$block10982~b: $Heap := $Heap[temp0, $inv := BasicMethodology]; goto $$block10982~a;
  $$block10982~a: assume IsHeap($Heap); goto block10914;
  block10914: goto block10931;
  block10931: goto block10948;
  block10948: goto block10812;
  block10812: goto block10829;
  block10829: goto block10846;
  block10846: return;
  
}

axiom (System.String <: System.String);
axiom ($BaseClass(System.String) == System.Object);
axiom ((System.String <: $BaseClass(System.String)) && (AsDirectSubClass(System.String, $BaseClass(System.String)) == System.String));
axiom ($IsImmutable(System.String) && ($AsImmutable(System.String) == System.String));
axiom (System.IComparable <: System.Object);
axiom $IsMemberlessType(System.IComparable);
axiom (System.String <: System.IComparable);
axiom (System.ICloneable <: System.Object);
axiom $IsMemberlessType(System.ICloneable);
axiom (System.String <: System.ICloneable);
axiom (System.IConvertible <: System.Object);
axiom $IsMemberlessType(System.IConvertible);
axiom (System.String <: System.IConvertible);
axiom (System.IComparable`1...System.String <: System.Object);
axiom $IsMemberlessType(System.IComparable`1...System.String);
axiom (System.String <: System.IComparable`1...System.String);
axiom (System.Collections.Generic.IEnumerable`1...System.Char <: System.Object);
axiom (System.Collections.IEnumerable <: System.Object);
axiom $IsMemberlessType(System.Collections.IEnumerable);
axiom (System.Collections.Generic.IEnumerable`1...System.Char <: System.Collections.IEnumerable);
axiom $IsMemberlessType(System.Collections.Generic.IEnumerable`1...System.Char);
axiom (System.String <: System.Collections.Generic.IEnumerable`1...System.Char);
axiom (System.String <: System.Collections.IEnumerable);
axiom (System.IEquatable`1...System.String <: System.Object);
axiom $IsMemberlessType(System.IEquatable`1...System.String);
axiom (System.String <: System.IEquatable`1...System.String);
axiom (forall $U : name :: {($U <: System.String)} (($U <: System.String) ==> ($U == System.String)));
axiom (ExtensibleComponent <: ExtensibleComponent);
axiom ($BaseClass(ExtensibleComponent) == System.Object);
axiom ((ExtensibleComponent <: $BaseClass(ExtensibleComponent)) && (AsDirectSubClass(ExtensibleComponent, $BaseClass(ExtensibleComponent)) == ExtensibleComponent));
axiom (!$IsImmutable(ExtensibleComponent) && ($AsMutable(ExtensibleComponent) == ExtensibleComponent));
procedure BasicMethodology..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation BasicMethodology..cctor() {
  entry: goto block11815;
  block11815: goto block11934;
  block11934: goto block11951;
  block11951: goto block11968;
  block11968: return;
  
}

axiom (SubClass <: SubClass);
axiom ($BaseClass(SubClass) == BasicMethodology);
axiom ((SubClass <: $BaseClass(SubClass)) && (AsDirectSubClass(SubClass, $BaseClass(SubClass)) == SubClass));
axiom (!$IsImmutable(SubClass) && ($AsMutable(SubClass) == SubClass));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: SubClass)} (((IsHeap($h) && ($h[$oi, $inv] <: SubClass)) && ($h[$oi, $localinv] != BasicMethodology)) ==> (30 <= $h[$oi, BasicMethodology.x])));
procedure SubClass.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation SubClass.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var return.value : bool where true;
  var stack50000o : ref;
  var stack0o : ref;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, SubClass); goto $$entry~f;
  $$entry~f: assume ($Heap[this, $allocated] == true); goto $$entry~e;
  $$entry~e: throwException := throwException$in; goto block12784;
  block12784: goto block12801;
  block12801: stack0i := 30; goto $$block12801~b;
  $$block12801~b: assert (this != null); goto $$block12801~a;
  $$block12801~a: stack1i := $Heap[this, BasicMethodology.x]; goto true12801to12920, false12801to12818;
  true12801to12920: assume (stack0i <= stack1i); goto block12920;
  false12801to12818: assume (stack0i > stack1i); goto block12818;
  block12920: goto block12937;
  block12818: stack0b := throwException; goto true12818to12869, false12818to12835;
  true12818to12869: assume !stack0b; goto block12869;
  false12818to12835: assume stack0b; goto block12835;
  block12869: return.value := false; goto block12971;
  block12835: assume false; goto $$block12835~i;
  $$block12835~i: havoc stack50000o; goto $$block12835~h;
  $$block12835~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block12835~g;
  $$block12835~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block12835~f;
  $$block12835~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block12835~e;
  $$block12835~e: assert (stack50000o != null); goto $$block12835~d;
  $$block12835~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block12835~c;
  $$block12835~c: stack0o := stack50000o; goto $$block12835~b;
  $$block12835~b: assert (stack0o != null); goto $$block12835~a;
  $$block12835~a: assume false; return;
  block12937: goto block12954;
  block12971: goto block12988;
  block12954: return.value := true; goto block12971;
  block12988: SS$Display.Return.Local := return.value; goto $$block12988~b;
  $$block12988~b: stack0b := return.value; goto $$block12988~a;
  $$block12988~a: $result := stack0b; return;
  
}

procedure SubClass..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == SubClass)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(SubClass <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation SubClass..ctor(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local15504 : ref where $Is(local15504, System.Exception);
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var stack0o : ref;
  var temp2 : ref;
  var temp3 : exposeVersionType;
  var local15538 : ref where $Is(local15538, System.Exception);
  var temp4 : ref;
  entry: assume $IsNotNull(this, SubClass); goto $$entry~h;
  $$entry~h: assume ($Heap[this, $allocated] == true); goto $$entry~g;
  $$entry~g: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto block14059;
  block14059: goto block14127;
  block14127: goto block14144;
  block14144: goto block14161;
  block14161: goto block14178;
  block14178: assert (this != null); goto $$block14178~c;
  $$block14178~c: call BasicMethodology..ctor(this); goto $$block14178~b;
  $$block14178~b: $Heap := $Heap[this, $NonNullFieldsAreInitialized := true]; goto $$block14178~a;
  $$block14178~a: assume IsHeap($Heap); goto block14297;
  block14297: goto block14314;
  block14314: goto block14331;
  block14331: temp0 := this; goto $$block14331~g;
  $$block14331~g: assert (temp0 != null); goto $$block14331~f;
  $$block14331~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == BasicMethodology)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block14331~e;
  $$block14331~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block14331~d;
  $$block14331~d: havoc temp1; goto $$block14331~c;
  $$block14331~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block14331~b;
  $$block14331~b: assume IsHeap($Heap); goto $$block14331~a;
  $$block14331~a: local15504 := null; goto block14348;
  block14348: assert (this != null); goto $$block14348~g;
  $$block14348~g: stack0i := $Heap[this, BasicMethodology.x]; goto $$block14348~f;
  $$block14348~f: stack1i := 20; goto $$block14348~e;
  $$block14348~e: stack0i := (stack0i + stack1i); goto $$block14348~d;
  $$block14348~d: assert (this != null); goto $$block14348~c;
  $$block14348~c: assert !($Heap[this, $inv] <: BasicMethodology); goto $$block14348~b;
  $$block14348~b: $Heap := $Heap[this, BasicMethodology.x := stack0i]; goto $$block14348~a;
  $$block14348~a: assume IsHeap($Heap); goto block14365;
  block14365: stack0i := 80; goto $$block14365~b;
  $$block14365~b: assert (this != null); goto $$block14365~a;
  $$block14365~a: stack1i := $Heap[this, BasicMethodology.x]; goto true14365to14399, false14365to14382;
  true14365to14399: assume (stack0i >= stack1i); goto block14399;
  false14365to14382: assume (stack0i < stack1i); goto block14382;
  block14399: goto block14416;
  block14382: stack0i := 80; goto $$block14382~d;
  $$block14382~d: assert (this != null); goto $$block14382~c;
  $$block14382~c: assert !($Heap[this, $inv] <: BasicMethodology); goto $$block14382~b;
  $$block14382~b: $Heap := $Heap[this, BasicMethodology.x := stack0i]; goto $$block14382~a;
  $$block14382~a: assume IsHeap($Heap); goto block14399;
  block14416: goto block14433;
  block14433: assert (this != null); goto $$block14433~e;
  $$block14433~e: stack0o := $Heap[this, BasicMethodology.c]; goto $$block14433~d;
  $$block14433~d: assert (stack0o != null); goto $$block14433~c;
  $$block14433~c: stack0i := $Heap[stack0o, Component.y]; goto $$block14433~b;
  $$block14433~b: assert (this != null); goto $$block14433~a;
  $$block14433~a: stack1i := $Heap[this, BasicMethodology.x]; goto true14433to14603, false14433to14450;
  true14433to14603: assume (stack0i >= stack1i); goto block14603;
  false14433to14450: assume (stack0i < stack1i); goto block14450;
  block14603: goto block14620;
  block14450: assert (this != null); goto $$block14450~i;
  $$block14450~i: stack0o := $Heap[this, BasicMethodology.c]; goto $$block14450~h;
  $$block14450~h: temp2 := stack0o; goto $$block14450~g;
  $$block14450~g: assert (temp2 != null); goto $$block14450~f;
  $$block14450~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] == Component)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block14450~e;
  $$block14450~e: $Heap := $Heap[temp2, $inv := System.Object]; goto $$block14450~d;
  $$block14450~d: havoc temp3; goto $$block14450~c;
  $$block14450~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block14450~b;
  $$block14450~b: assume IsHeap($Heap); goto $$block14450~a;
  $$block14450~a: local15538 := null; goto block14467;
  block14467: assert (this != null); goto $$block14467~f;
  $$block14467~f: stack0o := $Heap[this, BasicMethodology.c]; goto $$block14467~e;
  $$block14467~e: stack1i := 80; goto $$block14467~d;
  $$block14467~d: assert (stack0o != null); goto $$block14467~c;
  $$block14467~c: assert (!($Heap[stack0o, $inv] <: Component) || ($Heap[stack0o, $localinv] == System.Object)); goto $$block14467~b;
  $$block14467~b: $Heap := $Heap[stack0o, Component.y := stack1i]; goto $$block14467~a;
  $$block14467~a: assume IsHeap($Heap); goto block14807;
  block14620: goto block14637;
  block14807: stack0o := null; goto true14807to14909, false14807to14824;
  true14807to14909: assume (local15538 == stack0o); goto block14909;
  false14807to14824: assume (local15538 != stack0o); goto block14824;
  block14909: goto block14926;
  block14824: goto true14824to14909, false14824to14841;
  block14637: goto block15079;
  true14824to14909: assume ($As(local15538, Microsoft.Contracts.ICheckedException) != null); goto block14909;
  false14824to14841: assume ($As(local15538, Microsoft.Contracts.ICheckedException) == null); goto block14841;
  block14841: goto block14858;
  block15079: stack0o := null; goto true15079to15181, false15079to15096;
  true15079to15181: assume (local15504 == stack0o); goto block15181;
  false15079to15096: assume (local15504 != stack0o); goto block15096;
  block15181: goto block15198;
  block15096: goto true15096to15181, false15096to15113;
  block14926: assert (temp2 != null); goto $$block14926~e;
  $$block14926~e: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block14926~d;
  $$block14926~d: assert ($Heap[temp2, Component.y] <= 80); goto $$block14926~c;
  $$block14926~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Component)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block14926~b;
  $$block14926~b: $Heap := $Heap[temp2, $inv := Component]; goto $$block14926~a;
  $$block14926~a: assume IsHeap($Heap); goto block14858;
  true15096to15181: assume ($As(local15504, Microsoft.Contracts.ICheckedException) != null); goto block15181;
  false15096to15113: assume ($As(local15504, Microsoft.Contracts.ICheckedException) == null); goto block15113;
  block15113: goto block15130;
  block14858: goto block14875;
  block15198: assert (temp0 != null); goto $$block15198~f;
  $$block15198~f: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block15198~e;
  $$block15198~e: assert (10 <= $Heap[temp0, BasicMethodology.x]); goto $$block15198~d;
  $$block15198~d: assert ($Heap[temp0, BasicMethodology.x] <= $Heap[$Heap[temp0, BasicMethodology.c], Component.y]); goto $$block15198~c;
  $$block15198~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == BasicMethodology)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block15198~b;
  $$block15198~b: $Heap := $Heap[temp0, $inv := BasicMethodology]; goto $$block15198~a;
  $$block15198~a: assume IsHeap($Heap); goto block15130;
  block14875: goto block14892;
  block15130: goto block15147;
  block14892: goto block14586;
  block15147: goto block15164;
  block14586: goto block14603;
  block15164: goto block14756;
  block14756: goto block14773;
  block14773: goto block14790;
  block14790: temp4 := this; goto $$block14790~f;
  $$block14790~f: assert (temp4 != null); goto $$block14790~e;
  $$block14790~e: assert (($Heap[temp4, $inv] == BasicMethodology) && ($Heap[temp4, $localinv] == $typeof(temp4))); goto $$block14790~d;
  $$block14790~d: assert (30 <= $Heap[temp4, BasicMethodology.x]); goto $$block14790~c;
  $$block14790~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp4)) && ($Heap[$p, $ownerFrame] == SubClass)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block14790~b;
  $$block14790~b: $Heap := $Heap[temp4, $inv := SubClass]; goto $$block14790~a;
  $$block14790~a: assume IsHeap($Heap); return;
  
}

procedure BasicMethodology..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == BasicMethodology)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(BasicMethodology <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure SubClass.P(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == SubClass)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation SubClass.P(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local18785 : ref where $Is(local18785, System.Exception);
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var temp2 : ref;
  var temp3 : exposeVersionType;
  var local18819 : ref where $Is(local18819, System.Exception);
  var stack0o : ref;
  var temp4 : ref;
  var temp5 : exposeVersionType;
  var local18853 : ref where $Is(local18853, System.Exception);
  entry: assume $IsNotNull(this, SubClass); goto $$entry~i;
  $$entry~i: assume ($Heap[this, $allocated] == true); goto block16949;
  block16949: goto block17204;
  block17204: goto block17221;
  block17221: temp0 := this; goto $$block17221~g;
  $$block17221~g: assert (temp0 != null); goto $$block17221~f;
  $$block17221~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == SubClass)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block17221~e;
  $$block17221~e: $Heap := $Heap[temp0, $inv := BasicMethodology]; goto $$block17221~d;
  $$block17221~d: havoc temp1; goto $$block17221~c;
  $$block17221~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block17221~b;
  $$block17221~b: assume IsHeap($Heap); goto $$block17221~a;
  $$block17221~a: local18785 := null; goto block17238;
  block17238: assert (this != null); goto $$block17238~a;
  $$block17238~a: call BasicMethodology.P(this); goto block17255;
  block17255: assert (this != null); goto $$block17255~b;
  $$block17255~b: stack0i := $Heap[this, BasicMethodology.x]; goto $$block17255~a;
  $$block17255~a: stack1i := 30; goto true17255to17595, false17255to17272;
  true17255to17595: assume (stack0i >= stack1i); goto block17595;
  false17255to17272: assume (stack0i < stack1i); goto block17272;
  block17595: goto block17612;
  block17272: temp2 := this; goto $$block17272~g;
  $$block17272~g: assert (temp2 != null); goto $$block17272~f;
  $$block17272~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] == BasicMethodology)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block17272~e;
  $$block17272~e: $Heap := $Heap[temp2, $inv := System.Object]; goto $$block17272~d;
  $$block17272~d: havoc temp3; goto $$block17272~c;
  $$block17272~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block17272~b;
  $$block17272~b: assume IsHeap($Heap); goto $$block17272~a;
  $$block17272~a: local18819 := null; goto block17289;
  block17612: goto block17629;
  block17289: stack0i := 32; goto $$block17289~d;
  $$block17289~d: assert (this != null); goto $$block17289~c;
  $$block17289~c: assert !($Heap[this, $inv] <: BasicMethodology); goto $$block17289~b;
  $$block17289~b: $Heap := $Heap[this, BasicMethodology.x := stack0i]; goto $$block17289~a;
  $$block17289~a: assume IsHeap($Heap); goto block17306;
  block17629: goto block18343;
  block17306: assert (this != null); goto $$block17306~i;
  $$block17306~i: stack0o := $Heap[this, BasicMethodology.c]; goto $$block17306~h;
  $$block17306~h: temp4 := stack0o; goto $$block17306~g;
  $$block17306~g: assert (temp4 != null); goto $$block17306~f;
  $$block17306~f: assert ((((($Heap[temp4, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp4, $ownerRef], $inv] <: $Heap[temp4, $ownerFrame])) || ($Heap[$Heap[temp4, $ownerRef], $localinv] == $BaseClass($Heap[temp4, $ownerFrame]))) && ($Heap[temp4, $inv] == Component)) && ($Heap[temp4, $localinv] == $typeof(temp4))); goto $$block17306~e;
  $$block17306~e: $Heap := $Heap[temp4, $inv := System.Object]; goto $$block17306~d;
  $$block17306~d: havoc temp5; goto $$block17306~c;
  $$block17306~c: $Heap := $Heap[temp4, $exposeVersion := temp5]; goto $$block17306~b;
  $$block17306~b: assume IsHeap($Heap); goto $$block17306~a;
  $$block17306~a: local18853 := null; goto block17323;
  block18343: stack0o := null; goto true18343to18445, false18343to18360;
  true18343to18445: assume (local18785 == stack0o); goto block18445;
  false18343to18360: assume (local18785 != stack0o); goto block18360;
  block18445: goto block18462;
  block18360: goto true18360to18445, false18360to18377;
  block17323: assert (this != null); goto $$block17323~f;
  $$block17323~f: stack0o := $Heap[this, BasicMethodology.c]; goto $$block17323~e;
  $$block17323~e: stack1i := 32; goto $$block17323~d;
  $$block17323~d: assert (stack0o != null); goto $$block17323~c;
  $$block17323~c: assert (!($Heap[stack0o, $inv] <: Component) || ($Heap[stack0o, $localinv] == System.Object)); goto $$block17323~b;
  $$block17323~b: $Heap := $Heap[stack0o, Component.y := stack1i]; goto $$block17323~a;
  $$block17323~a: assume IsHeap($Heap); goto block17799;
  true18360to18445: assume ($As(local18785, Microsoft.Contracts.ICheckedException) != null); goto block18445;
  false18360to18377: assume ($As(local18785, Microsoft.Contracts.ICheckedException) == null); goto block18377;
  block18377: goto block18394;
  block17799: stack0o := null; goto true17799to17901, false17799to17816;
  true17799to17901: assume (local18853 == stack0o); goto block17901;
  false17799to17816: assume (local18853 != stack0o); goto block17816;
  block17901: goto block17918;
  block17816: goto true17816to17901, false17816to17833;
  block18462: assert (temp0 != null); goto $$block18462~e;
  $$block18462~e: assert (($Heap[temp0, $inv] == BasicMethodology) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block18462~d;
  $$block18462~d: assert (30 <= $Heap[temp0, BasicMethodology.x]); goto $$block18462~c;
  $$block18462~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == SubClass)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block18462~b;
  $$block18462~b: $Heap := $Heap[temp0, $inv := SubClass]; goto $$block18462~a;
  $$block18462~a: assume IsHeap($Heap); goto block18394;
  true17816to17901: assume ($As(local18853, Microsoft.Contracts.ICheckedException) != null); goto block17901;
  false17816to17833: assume ($As(local18853, Microsoft.Contracts.ICheckedException) == null); goto block17833;
  block17833: goto block17850;
  block18394: goto block18411;
  block17918: assert (temp4 != null); goto $$block17918~e;
  $$block17918~e: assert (($Heap[temp4, $inv] == System.Object) && ($Heap[temp4, $localinv] == $typeof(temp4))); goto $$block17918~d;
  $$block17918~d: assert ($Heap[temp4, Component.y] <= 80); goto $$block17918~c;
  $$block17918~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp4)) && ($Heap[$p, $ownerFrame] == Component)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block17918~b;
  $$block17918~b: $Heap := $Heap[temp4, $inv := Component]; goto $$block17918~a;
  $$block17918~a: assume IsHeap($Heap); goto block17850;
  block18411: goto block18428;
  block17850: goto block17867;
  block18428: goto block17748;
  block17867: goto block17884;
  block17748: goto block17765;
  block17884: goto block17442;
  block17765: goto block17782;
  block17442: goto block17459;
  block17782: return;
  block17459: goto block18071;
  block18071: stack0o := null; goto true18071to18173, false18071to18088;
  true18071to18173: assume (local18819 == stack0o); goto block18173;
  false18071to18088: assume (local18819 != stack0o); goto block18088;
  block18173: goto block18190;
  block18088: goto true18088to18173, false18088to18105;
  true18088to18173: assume ($As(local18819, Microsoft.Contracts.ICheckedException) != null); goto block18173;
  false18088to18105: assume ($As(local18819, Microsoft.Contracts.ICheckedException) == null); goto block18105;
  block18105: goto block18122;
  block18190: assert (temp2 != null); goto $$block18190~f;
  $$block18190~f: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block18190~e;
  $$block18190~e: assert (10 <= $Heap[temp2, BasicMethodology.x]); goto $$block18190~d;
  $$block18190~d: assert ($Heap[temp2, BasicMethodology.x] <= $Heap[$Heap[temp2, BasicMethodology.c], Component.y]); goto $$block18190~c;
  $$block18190~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == BasicMethodology)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block18190~b;
  $$block18190~b: $Heap := $Heap[temp2, $inv := BasicMethodology]; goto $$block18190~a;
  $$block18190~a: assume IsHeap($Heap); goto block18122;
  block18122: goto block18139;
  block18139: goto block18156;
  block18156: goto block17578;
  block17578: goto block17595;
  
}

procedure SubClass..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation SubClass..cctor() {
  entry: goto block19414;
  block19414: goto block19533;
  block19533: goto block19550;
  block19550: goto block19567;
  block19567: return;
  
}

procedure Component.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Component.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var return.value : bool where true;
  var stack50000o : ref;
  var stack0o : ref;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, Component); goto $$entry~k;
  $$entry~k: assume ($Heap[this, $allocated] == true); goto $$entry~j;
  $$entry~j: throwException := throwException$in; goto block20383;
  block20383: goto block20400;
  block20400: assert (this != null); goto $$block20400~b;
  $$block20400~b: stack0i := $Heap[this, Component.y]; goto $$block20400~a;
  $$block20400~a: stack1i := 80; goto true20400to20519, false20400to20417;
  true20400to20519: assume (stack0i <= stack1i); goto block20519;
  false20400to20417: assume (stack0i > stack1i); goto block20417;
  block20519: goto block20536;
  block20417: stack0b := throwException; goto true20417to20468, false20417to20434;
  true20417to20468: assume !stack0b; goto block20468;
  false20417to20434: assume stack0b; goto block20434;
  block20468: return.value := false; goto block20570;
  block20434: assume false; goto $$block20434~i;
  $$block20434~i: havoc stack50000o; goto $$block20434~h;
  $$block20434~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block20434~g;
  $$block20434~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block20434~f;
  $$block20434~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block20434~e;
  $$block20434~e: assert (stack50000o != null); goto $$block20434~d;
  $$block20434~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block20434~c;
  $$block20434~c: stack0o := stack50000o; goto $$block20434~b;
  $$block20434~b: assert (stack0o != null); goto $$block20434~a;
  $$block20434~a: assume false; return;
  block20536: goto block20553;
  block20570: goto block20587;
  block20553: return.value := true; goto block20570;
  block20587: SS$Display.Return.Local := return.value; goto $$block20587~b;
  $$block20587~b: stack0b := return.value; goto $$block20587~a;
  $$block20587~a: $result := stack0b; return;
  
}

procedure Component..ctor$System.Int32(this : ref, z$in : int where InRange(z$in, System.Int32));
  free requires true;
  requires (z$in <= 80);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ($Heap[this, Component.y] == z$in);
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Component)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Component <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation Component..ctor$System.Int32(this : ref, z$in : int) {
  var z : int where InRange(z, System.Int32);
  var temp0 : ref;
  entry: assume $IsNotNull(this, Component); goto $$entry~o;
  $$entry~o: assume ($Heap[this, $allocated] == true); goto $$entry~n;
  $$entry~n: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~m;
  $$entry~m: z := z$in; goto $$entry~l;
  $$entry~l: assume ($Heap[this, Component.y] == 0); goto block21403;
  block21403: goto block21607;
  block21607: goto block21624;
  block21624: goto block21641;
  block21641: goto block21658;
  block21658: assert (this != null); goto $$block21658~a;
  $$block21658~a: call System.Object..ctor(this); goto block21777;
  block21777: goto block21794;
  block21794: goto block21811;
  block21811: assert (this != null); goto $$block21811~c;
  $$block21811~c: assert (!($Heap[this, $inv] <: Component) || ($Heap[this, $localinv] == System.Object)); goto $$block21811~b;
  $$block21811~b: $Heap := $Heap[this, Component.y := z]; goto $$block21811~a;
  $$block21811~a: assume IsHeap($Heap); goto block21828;
  block21828: goto block21845;
  block21845: temp0 := this; goto $$block21845~f;
  $$block21845~f: assert (temp0 != null); goto $$block21845~e;
  $$block21845~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block21845~d;
  $$block21845~d: assert ($Heap[temp0, Component.y] <= 80); goto $$block21845~c;
  $$block21845~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Component)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block21845~b;
  $$block21845~b: $Heap := $Heap[temp0, $inv := Component]; goto $$block21845~a;
  $$block21845~a: assume IsHeap($Heap); goto block22049;
  block22049: goto block22066;
  block22066: return;
  
}

procedure System.Object..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(System.Object <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure Component..ctor$System.Int32$System.Boolean(this : ref, z$in : int where InRange(z$in, System.Int32), bad$in : bool where true);
  free requires true;
  free requires true;
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Component)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Component <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation Component..ctor$System.Int32$System.Boolean(this : ref, z$in : int, bad$in : bool) {
  var z : int where InRange(z, System.Int32);
  var bad : bool where true;
  var stack0b : bool;
  var stack0i : int;
  var temp0 : ref;
  entry: assume $IsNotNull(this, Component); goto $$entry~t;
  $$entry~t: assume ($Heap[this, $allocated] == true); goto $$entry~s;
  $$entry~s: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~r;
  $$entry~r: z := z$in; goto $$entry~q;
  $$entry~q: bad := bad$in; goto $$entry~p;
  $$entry~p: assume ($Heap[this, Component.y] == 0); goto block22542;
  block22542: goto block22559;
  block22559: goto block22576;
  block22576: goto block22593;
  block22593: assert (this != null); goto $$block22593~a;
  $$block22593~a: call System.Object..ctor(this); goto block22712;
  block22712: goto block22729;
  block22729: goto block22746;
  block22746: stack0b := bad; goto true22746to22780, false22746to22763;
  true22746to22780: assume !stack0b; goto block22780;
  false22746to22763: assume stack0b; goto block22763;
  block22780: goto block22797;
  block22763: stack0i := z; goto block22814;
  block22797: stack0i := 0; goto block22814;
  block22814: goto block22831;
  block22831: assert (this != null); goto $$block22831~c;
  $$block22831~c: assert (!($Heap[this, $inv] <: Component) || ($Heap[this, $localinv] == System.Object)); goto $$block22831~b;
  $$block22831~b: $Heap := $Heap[this, Component.y := stack0i]; goto $$block22831~a;
  $$block22831~a: assume IsHeap($Heap); goto block22848;
  block22848: goto block22865;
  block22865: temp0 := this; goto $$block22865~f;
  $$block22865~f: assert (temp0 != null); goto $$block22865~e;
  $$block22865~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block22865~d;
  $$block22865~d: assert ($Heap[temp0, Component.y] <= 80); goto $$block22865~c;
  $$block22865~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Component)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block22865~b;
  $$block22865~b: $Heap := $Heap[temp0, $inv := Component]; goto $$block22865~a;
  $$block22865~a: assume IsHeap($Heap); return;
  
}

procedure Component..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Component..cctor() {
  entry: goto block23460;
  block23460: goto block23579;
  block23579: goto block23596;
  block23596: goto block23613;
  block23613: return;
  
}

procedure ExtensibleComponent..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == ExtensibleComponent)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(ExtensibleComponent <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation ExtensibleComponent..ctor(this : ref) {
  entry: assume $IsNotNull(this, ExtensibleComponent); goto $$entry~v;
  $$entry~v: assume ($Heap[this, $allocated] == true); goto $$entry~u;
  $$entry~u: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto block24259;
  block24259: goto block24276;
  block24276: goto block24293;
  block24293: assert (this != null); goto $$block24293~a;
  $$block24293~a: call System.Object..ctor(this); goto block24310;
  block24310: goto block24327;
  block24327: assert (this != null); goto $$block24327~d;
  $$block24327~d: assert (($Heap[this, $inv] == System.Object) && ($Heap[this, $localinv] == $typeof(this))); goto $$block24327~c;
  $$block24327~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == this)) && ($Heap[$p, $ownerFrame] == ExtensibleComponent)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block24327~b;
  $$block24327~b: $Heap := $Heap[this, $inv := ExtensibleComponent]; goto $$block24327~a;
  $$block24327~a: assume IsHeap($Heap); return;
  
}

axiom (C <: C);
axiom ($BaseClass(C) == System.Object);
axiom ((C <: $BaseClass(C)) && (AsDirectSubClass(C, $BaseClass(C)) == C));
axiom (!$IsImmutable(C) && ($AsMutable(C) == C));
axiom (CS <: CS);
axiom ($BaseClass(CS) == C);
axiom ((CS <: $BaseClass(CS)) && (AsDirectSubClass(CS, $BaseClass(CS)) == CS));
axiom (!$IsImmutable(CS) && ($AsMutable(CS) == CS));
axiom (forall $U : name :: {($U <: CS)} (($U <: CS) ==> ($U == CS)));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: CS)} (((IsHeap($h) && ($h[$oi, $inv] <: CS)) && ($h[$oi, $localinv] != C)) ==> ($h[$oi, CS.f] != 0)));
axiom (forall $U : name :: {($U <: C)} (($U <: C) ==> (($U == C) || ($U <: CS))));
procedure C.foo(this : ref) returns ($result : int where InRange($result, System.Int32));
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == C)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures InRange($result, System.Int32);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C.foo(this : ref) returns ($result : int) {
  var return.value : int where InRange(return.value, System.Int32);
  var SS$Display.Return.Local : int where InRange(SS$Display.Return.Local, System.Int32);
  var stack0i : int;
  entry: assume $IsNotNull(this, C); goto $$entry~w;
  $$entry~w: assume ($Heap[this, $allocated] == true); goto block24480;
  block24480: goto block24497;
  block24497: return.value := 5; goto block24514;
  block24514: goto block24531;
  block24531: SS$Display.Return.Local := return.value; goto $$block24531~b;
  $$block24531~b: stack0i := return.value; goto $$block24531~a;
  $$block24531~a: $result := stack0i; return;
  
}

procedure C..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == C)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(C <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation C..ctor(this : ref) {
  entry: assume $IsNotNull(this, C); goto $$entry~y;
  $$entry~y: assume ($Heap[this, $allocated] == true); goto $$entry~x;
  $$entry~x: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto block24701;
  block24701: goto block24718;
  block24718: goto block24735;
  block24735: assert (this != null); goto $$block24735~a;
  $$block24735~a: call System.Object..ctor(this); goto block24752;
  block24752: goto block24769;
  block24769: assert (this != null); goto $$block24769~d;
  $$block24769~d: assert (($Heap[this, $inv] == System.Object) && ($Heap[this, $localinv] == $typeof(this))); goto $$block24769~c;
  $$block24769~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == this)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block24769~b;
  $$block24769~b: $Heap := $Heap[this, $inv := C]; goto $$block24769~a;
  $$block24769~a: assume IsHeap($Heap); return;
  
}

procedure CS.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation CS.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var stack50000o : ref;
  var stack0o : ref;
  var return.value : bool where true;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, CS); goto $$entry~aa;
  $$entry~aa: assume ($Heap[this, $allocated] == true); goto $$entry~z;
  $$entry~z: throwException := throwException$in; goto block25075;
  block25075: goto block25092;
  block25092: assert (this != null); goto $$block25092~b;
  $$block25092~b: stack0i := $Heap[this, CS.f]; goto $$block25092~a;
  $$block25092~a: stack1i := 0; goto true25092to25211, false25092to25109;
  true25092to25211: assume (stack0i != stack1i); goto block25211;
  false25092to25109: assume (stack0i == stack1i); goto block25109;
  block25211: goto block25228;
  block25109: stack0b := throwException; goto true25109to25160, false25109to25126;
  true25109to25160: assume !stack0b; goto block25160;
  false25109to25126: assume stack0b; goto block25126;
  block25160: return.value := false; goto block25262;
  block25126: assume false; goto $$block25126~i;
  $$block25126~i: havoc stack50000o; goto $$block25126~h;
  $$block25126~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block25126~g;
  $$block25126~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block25126~f;
  $$block25126~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block25126~e;
  $$block25126~e: assert (stack50000o != null); goto $$block25126~d;
  $$block25126~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block25126~c;
  $$block25126~c: stack0o := stack50000o; goto $$block25126~b;
  $$block25126~b: assert (stack0o != null); goto $$block25126~a;
  $$block25126~a: assume false; return;
  block25228: goto block25245;
  block25245: return.value := true; goto block25262;
  block25262: goto block25279;
  block25279: SS$Display.Return.Local := return.value; goto $$block25279~b;
  $$block25279~b: stack0b := return.value; goto $$block25279~a;
  $$block25279~a: $result := stack0b; return;
  
}

procedure CS.foo(this : ref) returns ($result : int where InRange($result, System.Int32));
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == CS)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures InRange($result, System.Int32);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation CS.foo(this : ref) returns ($result : int) {
  var stack0i : int;
  var stack1i : int;
  var return.value : int where InRange(return.value, System.Int32);
  var SS$Display.Return.Local : int where InRange(SS$Display.Return.Local, System.Int32);
  entry: assume $IsNotNull(this, CS); goto $$entry~ab;
  $$entry~ab: assume ($Heap[this, $allocated] == true); goto block25721;
  block25721: goto block25925;
  block25925: goto block25942;
  block25942: stack0i := 5; goto $$block25942~e;
  $$block25942~e: assert (this != null); goto $$block25942~d;
  $$block25942~d: stack1i := $Heap[this, CS.f]; goto $$block25942~c;
  $$block25942~c: assert (stack1i != 0); goto $$block25942~b;
  $$block25942~b: stack0i := (stack0i / stack1i); goto $$block25942~a;
  $$block25942~a: return.value := stack0i; goto block25959;
  block25959: goto block25976;
  block25976: SS$Display.Return.Local := return.value; goto $$block25976~b;
  $$block25976~b: stack0i := return.value; goto $$block25976~a;
  $$block25976~a: $result := stack0i; return;
  
}

procedure CS..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == CS)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(CS <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation CS..ctor(this : ref) {
  var stack0i : int;
  var temp0 : ref;
  entry: assume $IsNotNull(this, CS); goto $$entry~ae;
  $$entry~ae: assume ($Heap[this, $allocated] == true); goto $$entry~ad;
  $$entry~ad: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~ac;
  $$entry~ac: assume ($Heap[this, CS.f] == 0); goto block26350;
  block26350: goto block26367;
  block26367: goto block26384;
  block26384: goto block26401;
  block26401: goto block26418;
  block26418: stack0i := 1; goto $$block26418~d;
  $$block26418~d: assert (this != null); goto $$block26418~c;
  $$block26418~c: assert (!($Heap[this, $inv] <: CS) || ($Heap[this, $localinv] == C)); goto $$block26418~b;
  $$block26418~b: $Heap := $Heap[this, CS.f := stack0i]; goto $$block26418~a;
  $$block26418~a: assume IsHeap($Heap); goto block26435;
  block26435: assert (this != null); goto $$block26435~a;
  $$block26435~a: call C..ctor(this); goto block26554;
  block26554: goto block26571;
  block26571: goto block26588;
  block26588: goto block26605;
  block26605: temp0 := this; goto $$block26605~f;
  $$block26605~f: assert (temp0 != null); goto $$block26605~e;
  $$block26605~e: assert (($Heap[temp0, $inv] == C) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block26605~d;
  $$block26605~d: assert ($Heap[temp0, CS.f] != 0); goto $$block26605~c;
  $$block26605~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == CS)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block26605~b;
  $$block26605~b: $Heap := $Heap[temp0, $inv := CS]; goto $$block26605~a;
  $$block26605~a: assume IsHeap($Heap); return;
  
}

procedure CS.test0();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation CS.test0() {
  var stack50000o : ref;
  var stack0o : ref;
  var t : ref where $Is(t, C);
  entry: goto block26979;
  block26979: goto block26996;
  block26996: havoc stack50000o; goto $$block26996~g;
  $$block26996~g: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == CS)); goto $$block26996~f;
  $$block26996~f: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block26996~e;
  $$block26996~e: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block26996~d;
  $$block26996~d: assert (stack50000o != null); goto $$block26996~c;
  $$block26996~c: call CS..ctor(stack50000o); goto $$block26996~b;
  $$block26996~b: stack0o := stack50000o; goto $$block26996~a;
  $$block26996~a: t := stack0o; goto block27013;
  block27013: assert ((((($Heap[t, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[t, $ownerRef], $inv] <: $Heap[t, $ownerFrame])) || ($Heap[$Heap[t, $ownerRef], $localinv] == $BaseClass($Heap[t, $ownerFrame]))) && ($Heap[t, $inv] == C)) && ($Heap[t, $localinv] == $typeof(t))); goto block27166;
  block27166: goto block27183;
  block27183: goto block27200;
  block27200: return;
  
}

procedure CS.test1();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation CS.test1() {
  var stack50000o : ref;
  var stack0o : ref;
  var t : ref where $Is(t, C);
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local28543 : ref where $Is(local28543, System.Exception);
  var local28560 : ref where $Is(local28560, C);
  var stack1s : struct;
  var stack1o : ref;
  var temp2 : exposeVersionType;
  var stack1i : int;
  var stack0i : int;
  var stack0b : bool;
  entry: goto block27812;
  block27812: goto block27880;
  block27880: havoc stack50000o; goto $$block27880~g;
  $$block27880~g: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == CS)); goto $$block27880~f;
  $$block27880~f: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block27880~e;
  $$block27880~e: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block27880~d;
  $$block27880~d: assert (stack50000o != null); goto $$block27880~c;
  $$block27880~c: call CS..ctor(stack50000o); goto $$block27880~b;
  $$block27880~b: stack0o := stack50000o; goto $$block27880~a;
  $$block27880~a: t := stack0o; goto block27897;
  block27897: assert $Is(t, CS); goto $$block27897~i;
  $$block27897~i: stack0o := t; goto $$block27897~h;
  $$block27897~h: temp0 := stack0o; goto $$block27897~g;
  $$block27897~g: assert (temp0 != null); goto $$block27897~f;
  $$block27897~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == CS)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block27897~e;
  $$block27897~e: $Heap := $Heap[temp0, $inv := C]; goto $$block27897~d;
  $$block27897~d: havoc temp1; goto $$block27897~c;
  $$block27897~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block27897~b;
  $$block27897~b: assume IsHeap($Heap); goto $$block27897~a;
  $$block27897~a: local28543 := null; goto block27914;
  block27914: local28560 := t; goto $$block27914~j;
  $$block27914~j: stack0o := local28560; goto $$block27914~i;
  $$block27914~i: havoc stack1s; goto $$block27914~h;
  $$block27914~h: assume $IsTokenForType(stack1s, C); goto $$block27914~g;
  $$block27914~g: stack1o := TypeObject(C); goto $$block27914~f;
  $$block27914~f: assert (stack0o != null); goto $$block27914~e;
  $$block27914~e: assert ((((($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame])) || ($Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame]))) && ($Heap[stack0o, $inv] == C)) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block27914~d;
  $$block27914~d: $Heap := $Heap[stack0o, $inv := System.Object]; goto $$block27914~c;
  $$block27914~c: havoc temp2; goto $$block27914~b;
  $$block27914~b: $Heap := $Heap[stack0o, $exposeVersion := temp2]; goto $$block27914~a;
  $$block27914~a: assume IsHeap($Heap); goto block27931;
  block27931: assert $Is(t, CS); goto $$block27931~o;
  $$block27931~o: stack0o := t; goto $$block27931~n;
  $$block27931~n: stack1i := 0; goto $$block27931~m;
  $$block27931~m: assert (stack0o != null); goto $$block27931~l;
  $$block27931~l: assert (!($Heap[stack0o, $inv] <: CS) || ($Heap[stack0o, $localinv] == C)); goto $$block27931~k;
  $$block27931~k: $Heap := $Heap[stack0o, CS.f := stack1i]; goto $$block27931~j;
  $$block27931~j: assume IsHeap($Heap); goto $$block27931~i;
  $$block27931~i: assert (t != null); goto $$block27931~h;
  $$block27931~h: call stack0i := C.foo$.Virtual.$(t); goto $$block27931~g;
  $$block27931~g: assert $Is(t, CS); goto $$block27931~f;
  $$block27931~f: stack0o := t; goto $$block27931~e;
  $$block27931~e: stack1i := 1; goto $$block27931~d;
  $$block27931~d: assert (stack0o != null); goto $$block27931~c;
  $$block27931~c: assert (!($Heap[stack0o, $inv] <: CS) || ($Heap[stack0o, $localinv] == C)); goto $$block27931~b;
  $$block27931~b: $Heap := $Heap[stack0o, CS.f := stack1i]; goto $$block27931~a;
  $$block27931~a: assume IsHeap($Heap); goto block28169;
  block28169: stack0o := local28560; goto $$block28169~h;
  $$block28169~h: havoc stack1s; goto $$block28169~g;
  $$block28169~g: assume $IsTokenForType(stack1s, C); goto $$block28169~f;
  $$block28169~f: stack1o := TypeObject(C); goto $$block28169~e;
  $$block28169~e: assert (stack0o != null); goto $$block28169~d;
  $$block28169~d: assert (($Heap[stack0o, $inv] == System.Object) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block28169~c;
  $$block28169~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == stack0o)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block28169~b;
  $$block28169~b: $Heap := $Heap[stack0o, $inv := C]; goto $$block28169~a;
  $$block28169~a: assume IsHeap($Heap); goto block27982;
  block27982: goto block27999;
  block27999: goto block28186;
  block28186: stack0o := null; goto true28186to28288, false28186to28203;
  true28186to28288: assume (local28543 == stack0o); goto block28288;
  false28186to28203: assume (local28543 != stack0o); goto block28203;
  block28288: goto block28305;
  block28203: goto true28203to28288, false28203to28220;
  true28203to28288: assume ($As(local28543, Microsoft.Contracts.ICheckedException) != null); goto block28288;
  false28203to28220: assume ($As(local28543, Microsoft.Contracts.ICheckedException) == null); goto block28220;
  block28220: goto block28237;
  block28305: assert (temp0 != null); goto $$block28305~e;
  $$block28305~e: assert (($Heap[temp0, $inv] == C) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block28305~d;
  $$block28305~d: assert ($Heap[temp0, CS.f] != 0); goto $$block28305~c;
  $$block28305~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == CS)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block28305~b;
  $$block28305~b: $Heap := $Heap[temp0, $inv := CS]; goto $$block28305~a;
  $$block28305~a: assume IsHeap($Heap); goto block28237;
  block28237: goto block28254;
  block28254: goto block28271;
  block28271: goto block28118;
  block28118: goto block28135;
  block28135: goto block28152;
  block28152: return;
  
}

axiom (System.Type <: System.Type);
axiom (System.Reflection.MemberInfo <: System.Reflection.MemberInfo);
axiom ($BaseClass(System.Reflection.MemberInfo) == System.Object);
axiom ((System.Reflection.MemberInfo <: $BaseClass(System.Reflection.MemberInfo)) && (AsDirectSubClass(System.Reflection.MemberInfo, $BaseClass(System.Reflection.MemberInfo)) == System.Reflection.MemberInfo));
axiom ($IsImmutable(System.Reflection.MemberInfo) && ($AsImmutable(System.Reflection.MemberInfo) == System.Reflection.MemberInfo));
axiom (System.Reflection.ICustomAttributeProvider <: System.Object);
axiom $IsMemberlessType(System.Reflection.ICustomAttributeProvider);
axiom (System.Reflection.MemberInfo <: System.Reflection.ICustomAttributeProvider);
axiom (System.Runtime.InteropServices._MemberInfo <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._MemberInfo);
axiom (System.Reflection.MemberInfo <: System.Runtime.InteropServices._MemberInfo);
axiom $IsMemberlessType(System.Reflection.MemberInfo);
axiom ($BaseClass(System.Type) == System.Reflection.MemberInfo);
axiom ((System.Type <: $BaseClass(System.Type)) && (AsDirectSubClass(System.Type, $BaseClass(System.Type)) == System.Type));
axiom ($IsImmutable(System.Type) && ($AsImmutable(System.Type) == System.Type));
axiom (System.Runtime.InteropServices._Type <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Type);
axiom (System.Type <: System.Runtime.InteropServices._Type);
axiom (System.Reflection.IReflect <: System.Object);
axiom $IsMemberlessType(System.Reflection.IReflect);
axiom (System.Type <: System.Reflection.IReflect);
axiom $IsMemberlessType(System.Type);
procedure C.foo$.Virtual.$(this : ref) returns ($result : int where InRange($result, System.Int32));
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == $typeof(this))) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures InRange($result, System.Int32);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

procedure CS.test2();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation CS.test2() {
  var stack50000o : ref;
  var stack0o : ref;
  var t : ref where $Is(t, C);
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local30821 : ref where $Is(local30821, System.Exception);
  var local30838 : ref where $Is(local30838, C);
  var stack1s : struct;
  var stack1o : ref;
  var temp2 : exposeVersionType;
  var stack1i : int;
  var stack0b : bool;
  var stack0i : int;
  var temp3 : ref;
  var temp4 : exposeVersionType;
  var local30923 : ref where $Is(local30923, System.Exception);
  var local30940 : ref where $Is(local30940, C);
  var temp5 : exposeVersionType;
  entry: goto block29495;
  block29495: goto block29563;
  block29563: havoc stack50000o; goto $$block29563~g;
  $$block29563~g: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == CS)); goto $$block29563~f;
  $$block29563~f: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block29563~e;
  $$block29563~e: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block29563~d;
  $$block29563~d: assert (stack50000o != null); goto $$block29563~c;
  $$block29563~c: call CS..ctor(stack50000o); goto $$block29563~b;
  $$block29563~b: stack0o := stack50000o; goto $$block29563~a;
  $$block29563~a: t := stack0o; goto block29580;
  block29580: assert $Is(t, CS); goto $$block29580~i;
  $$block29580~i: stack0o := t; goto $$block29580~h;
  $$block29580~h: temp0 := stack0o; goto $$block29580~g;
  $$block29580~g: assert (temp0 != null); goto $$block29580~f;
  $$block29580~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == CS)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block29580~e;
  $$block29580~e: $Heap := $Heap[temp0, $inv := C]; goto $$block29580~d;
  $$block29580~d: havoc temp1; goto $$block29580~c;
  $$block29580~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block29580~b;
  $$block29580~b: assume IsHeap($Heap); goto $$block29580~a;
  $$block29580~a: local30821 := null; goto block29597;
  block29597: local30838 := t; goto $$block29597~j;
  $$block29597~j: stack0o := local30838; goto $$block29597~i;
  $$block29597~i: havoc stack1s; goto $$block29597~h;
  $$block29597~h: assume $IsTokenForType(stack1s, C); goto $$block29597~g;
  $$block29597~g: stack1o := TypeObject(C); goto $$block29597~f;
  $$block29597~f: assert (stack0o != null); goto $$block29597~e;
  $$block29597~e: assert ((((($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame])) || ($Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame]))) && ($Heap[stack0o, $inv] == C)) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block29597~d;
  $$block29597~d: $Heap := $Heap[stack0o, $inv := System.Object]; goto $$block29597~c;
  $$block29597~c: havoc temp2; goto $$block29597~b;
  $$block29597~b: $Heap := $Heap[stack0o, $exposeVersion := temp2]; goto $$block29597~a;
  $$block29597~a: assume IsHeap($Heap); goto block29614;
  block29614: assert $Is(t, CS); goto $$block29614~f;
  $$block29614~f: stack0o := t; goto $$block29614~e;
  $$block29614~e: stack1i := 0; goto $$block29614~d;
  $$block29614~d: assert (stack0o != null); goto $$block29614~c;
  $$block29614~c: assert (!($Heap[stack0o, $inv] <: CS) || ($Heap[stack0o, $localinv] == C)); goto $$block29614~b;
  $$block29614~b: $Heap := $Heap[stack0o, CS.f := stack1i]; goto $$block29614~a;
  $$block29614~a: assume IsHeap($Heap); goto block30107;
  block30107: stack0o := local30838; goto $$block30107~h;
  $$block30107~h: havoc stack1s; goto $$block30107~g;
  $$block30107~g: assume $IsTokenForType(stack1s, C); goto $$block30107~f;
  $$block30107~f: stack1o := TypeObject(C); goto $$block30107~e;
  $$block30107~e: assert (stack0o != null); goto $$block30107~d;
  $$block30107~d: assert (($Heap[stack0o, $inv] == System.Object) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block30107~c;
  $$block30107~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == stack0o)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block30107~b;
  $$block30107~b: $Heap := $Heap[stack0o, $inv := C]; goto $$block30107~a;
  $$block30107~a: assume IsHeap($Heap); goto block29665;
  block29665: goto block29682;
  block29682: goto block30124;
  block30124: stack0o := null; goto true30124to30226, false30124to30141;
  true30124to30226: assume (local30821 == stack0o); goto block30226;
  false30124to30141: assume (local30821 != stack0o); goto block30141;
  block30226: goto block30243;
  block30141: goto true30141to30226, false30141to30158;
  true30141to30226: assume ($As(local30821, Microsoft.Contracts.ICheckedException) != null); goto block30226;
  false30141to30158: assume ($As(local30821, Microsoft.Contracts.ICheckedException) == null); goto block30158;
  block30158: goto block30175;
  block30243: assert (temp0 != null); goto $$block30243~e;
  $$block30243~e: assert (($Heap[temp0, $inv] == C) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block30243~d;
  $$block30243~d: assert ($Heap[temp0, CS.f] != 0); goto $$block30243~c;
  $$block30243~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == CS)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block30243~b;
  $$block30243~b: $Heap := $Heap[temp0, $inv := CS]; goto $$block30243~a;
  $$block30243~a: assume IsHeap($Heap); goto block30175;
  block30175: goto block30192;
  block30192: goto block30209;
  block30209: goto block29801;
  block29801: goto block29818;
  block29818: assert (t != null); goto $$block29818~a;
  $$block29818~a: call stack0i := C.foo$.Virtual.$(t); goto block29835;
  block29835: assert $Is(t, CS); goto $$block29835~i;
  $$block29835~i: stack0o := t; goto $$block29835~h;
  $$block29835~h: temp3 := stack0o; goto $$block29835~g;
  $$block29835~g: assert (temp3 != null); goto $$block29835~f;
  $$block29835~f: assert ((((($Heap[temp3, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp3, $ownerRef], $inv] <: $Heap[temp3, $ownerFrame])) || ($Heap[$Heap[temp3, $ownerRef], $localinv] == $BaseClass($Heap[temp3, $ownerFrame]))) && ($Heap[temp3, $inv] == CS)) && ($Heap[temp3, $localinv] == $typeof(temp3))); goto $$block29835~e;
  $$block29835~e: $Heap := $Heap[temp3, $inv := C]; goto $$block29835~d;
  $$block29835~d: havoc temp4; goto $$block29835~c;
  $$block29835~c: $Heap := $Heap[temp3, $exposeVersion := temp4]; goto $$block29835~b;
  $$block29835~b: assume IsHeap($Heap); goto $$block29835~a;
  $$block29835~a: local30923 := null; goto block29852;
  block29852: local30940 := t; goto $$block29852~j;
  $$block29852~j: stack0o := local30940; goto $$block29852~i;
  $$block29852~i: havoc stack1s; goto $$block29852~h;
  $$block29852~h: assume $IsTokenForType(stack1s, C); goto $$block29852~g;
  $$block29852~g: stack1o := TypeObject(C); goto $$block29852~f;
  $$block29852~f: assert (stack0o != null); goto $$block29852~e;
  $$block29852~e: assert ((((($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame])) || ($Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame]))) && ($Heap[stack0o, $inv] == C)) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block29852~d;
  $$block29852~d: $Heap := $Heap[stack0o, $inv := System.Object]; goto $$block29852~c;
  $$block29852~c: havoc temp5; goto $$block29852~b;
  $$block29852~b: $Heap := $Heap[stack0o, $exposeVersion := temp5]; goto $$block29852~a;
  $$block29852~a: assume IsHeap($Heap); goto block29869;
  block29869: assert $Is(t, CS); goto $$block29869~f;
  $$block29869~f: stack0o := t; goto $$block29869~e;
  $$block29869~e: stack1i := 1; goto $$block29869~d;
  $$block29869~d: assert (stack0o != null); goto $$block29869~c;
  $$block29869~c: assert (!($Heap[stack0o, $inv] <: CS) || ($Heap[stack0o, $localinv] == C)); goto $$block29869~b;
  $$block29869~b: $Heap := $Heap[stack0o, CS.f := stack1i]; goto $$block29869~a;
  $$block29869~a: assume IsHeap($Heap); goto block30396;
  block30396: stack0o := local30940; goto $$block30396~h;
  $$block30396~h: havoc stack1s; goto $$block30396~g;
  $$block30396~g: assume $IsTokenForType(stack1s, C); goto $$block30396~f;
  $$block30396~f: stack1o := TypeObject(C); goto $$block30396~e;
  $$block30396~e: assert (stack0o != null); goto $$block30396~d;
  $$block30396~d: assert (($Heap[stack0o, $inv] == System.Object) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block30396~c;
  $$block30396~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == stack0o)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block30396~b;
  $$block30396~b: $Heap := $Heap[stack0o, $inv := C]; goto $$block30396~a;
  $$block30396~a: assume IsHeap($Heap); goto block29920;
  block29920: goto block29937;
  block29937: goto block30413;
  block30413: stack0o := null; goto true30413to30515, false30413to30430;
  true30413to30515: assume (local30923 == stack0o); goto block30515;
  false30413to30430: assume (local30923 != stack0o); goto block30430;
  block30515: goto block30532;
  block30430: goto true30430to30515, false30430to30447;
  true30430to30515: assume ($As(local30923, Microsoft.Contracts.ICheckedException) != null); goto block30515;
  false30430to30447: assume ($As(local30923, Microsoft.Contracts.ICheckedException) == null); goto block30447;
  block30447: goto block30464;
  block30532: assert (temp3 != null); goto $$block30532~e;
  $$block30532~e: assert (($Heap[temp3, $inv] == C) && ($Heap[temp3, $localinv] == $typeof(temp3))); goto $$block30532~d;
  $$block30532~d: assert ($Heap[temp3, CS.f] != 0); goto $$block30532~c;
  $$block30532~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp3)) && ($Heap[$p, $ownerFrame] == CS)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block30532~b;
  $$block30532~b: $Heap := $Heap[temp3, $inv := CS]; goto $$block30532~a;
  $$block30532~a: assume IsHeap($Heap); goto block30464;
  block30464: goto block30481;
  block30481: goto block30498;
  block30498: goto block30056;
  block30056: goto block30073;
  block30073: goto block30090;
  block30090: return;
  
}

procedure CS.test3();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation CS.test3() {
  var stack50000o : ref;
  var stack0o : ref;
  var t : ref where $Is(t, C);
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local33184 : ref where $Is(local33184, System.Exception);
  var local33201 : ref where $Is(local33201, C);
  var stack1s : struct;
  var stack1o : ref;
  var temp2 : exposeVersionType;
  var stack1i : int;
  var stack0b : bool;
  var stack0i : int;
  var temp3 : ref;
  var temp4 : exposeVersionType;
  var local33286 : ref where $Is(local33286, System.Exception);
  var local33303 : ref where $Is(local33303, C);
  var temp5 : exposeVersionType;
  entry: goto block31858;
  block31858: goto block31926;
  block31926: havoc stack50000o; goto $$block31926~g;
  $$block31926~g: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == CS)); goto $$block31926~f;
  $$block31926~f: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block31926~e;
  $$block31926~e: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block31926~d;
  $$block31926~d: assert (stack50000o != null); goto $$block31926~c;
  $$block31926~c: call CS..ctor(stack50000o); goto $$block31926~b;
  $$block31926~b: stack0o := stack50000o; goto $$block31926~a;
  $$block31926~a: t := stack0o; goto block31943;
  block31943: assert $Is(t, CS); goto $$block31943~i;
  $$block31943~i: stack0o := t; goto $$block31943~h;
  $$block31943~h: temp0 := stack0o; goto $$block31943~g;
  $$block31943~g: assert (temp0 != null); goto $$block31943~f;
  $$block31943~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == CS)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block31943~e;
  $$block31943~e: $Heap := $Heap[temp0, $inv := C]; goto $$block31943~d;
  $$block31943~d: havoc temp1; goto $$block31943~c;
  $$block31943~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block31943~b;
  $$block31943~b: assume IsHeap($Heap); goto $$block31943~a;
  $$block31943~a: local33184 := null; goto block31960;
  block31960: local33201 := t; goto $$block31960~j;
  $$block31960~j: stack0o := local33201; goto $$block31960~i;
  $$block31960~i: havoc stack1s; goto $$block31960~h;
  $$block31960~h: assume $IsTokenForType(stack1s, C); goto $$block31960~g;
  $$block31960~g: stack1o := TypeObject(C); goto $$block31960~f;
  $$block31960~f: assert (stack0o != null); goto $$block31960~e;
  $$block31960~e: assert ((((($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame])) || ($Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame]))) && ($Heap[stack0o, $inv] == C)) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block31960~d;
  $$block31960~d: $Heap := $Heap[stack0o, $inv := System.Object]; goto $$block31960~c;
  $$block31960~c: havoc temp2; goto $$block31960~b;
  $$block31960~b: $Heap := $Heap[stack0o, $exposeVersion := temp2]; goto $$block31960~a;
  $$block31960~a: assume IsHeap($Heap); goto block31977;
  block31977: assert $Is(t, CS); goto $$block31977~f;
  $$block31977~f: stack0o := t; goto $$block31977~e;
  $$block31977~e: stack1i := -1; goto $$block31977~d;
  $$block31977~d: assert (stack0o != null); goto $$block31977~c;
  $$block31977~c: assert (!($Heap[stack0o, $inv] <: CS) || ($Heap[stack0o, $localinv] == C)); goto $$block31977~b;
  $$block31977~b: $Heap := $Heap[stack0o, CS.f := stack1i]; goto $$block31977~a;
  $$block31977~a: assume IsHeap($Heap); goto block32470;
  block32470: stack0o := local33201; goto $$block32470~h;
  $$block32470~h: havoc stack1s; goto $$block32470~g;
  $$block32470~g: assume $IsTokenForType(stack1s, C); goto $$block32470~f;
  $$block32470~f: stack1o := TypeObject(C); goto $$block32470~e;
  $$block32470~e: assert (stack0o != null); goto $$block32470~d;
  $$block32470~d: assert (($Heap[stack0o, $inv] == System.Object) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block32470~c;
  $$block32470~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == stack0o)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block32470~b;
  $$block32470~b: $Heap := $Heap[stack0o, $inv := C]; goto $$block32470~a;
  $$block32470~a: assume IsHeap($Heap); goto block32028;
  block32028: goto block32045;
  block32045: goto block32487;
  block32487: stack0o := null; goto true32487to32589, false32487to32504;
  true32487to32589: assume (local33184 == stack0o); goto block32589;
  false32487to32504: assume (local33184 != stack0o); goto block32504;
  block32589: goto block32606;
  block32504: goto true32504to32589, false32504to32521;
  true32504to32589: assume ($As(local33184, Microsoft.Contracts.ICheckedException) != null); goto block32589;
  false32504to32521: assume ($As(local33184, Microsoft.Contracts.ICheckedException) == null); goto block32521;
  block32521: goto block32538;
  block32606: assert (temp0 != null); goto $$block32606~e;
  $$block32606~e: assert (($Heap[temp0, $inv] == C) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block32606~d;
  $$block32606~d: assert ($Heap[temp0, CS.f] != 0); goto $$block32606~c;
  $$block32606~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == CS)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block32606~b;
  $$block32606~b: $Heap := $Heap[temp0, $inv := CS]; goto $$block32606~a;
  $$block32606~a: assume IsHeap($Heap); goto block32538;
  block32538: goto block32555;
  block32555: goto block32572;
  block32572: goto block32164;
  block32164: goto block32181;
  block32181: assert (t != null); goto $$block32181~a;
  $$block32181~a: call stack0i := C.foo$.Virtual.$(t); goto block32198;
  block32198: assert $Is(t, CS); goto $$block32198~i;
  $$block32198~i: stack0o := t; goto $$block32198~h;
  $$block32198~h: temp3 := stack0o; goto $$block32198~g;
  $$block32198~g: assert (temp3 != null); goto $$block32198~f;
  $$block32198~f: assert ((((($Heap[temp3, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp3, $ownerRef], $inv] <: $Heap[temp3, $ownerFrame])) || ($Heap[$Heap[temp3, $ownerRef], $localinv] == $BaseClass($Heap[temp3, $ownerFrame]))) && ($Heap[temp3, $inv] == CS)) && ($Heap[temp3, $localinv] == $typeof(temp3))); goto $$block32198~e;
  $$block32198~e: $Heap := $Heap[temp3, $inv := C]; goto $$block32198~d;
  $$block32198~d: havoc temp4; goto $$block32198~c;
  $$block32198~c: $Heap := $Heap[temp3, $exposeVersion := temp4]; goto $$block32198~b;
  $$block32198~b: assume IsHeap($Heap); goto $$block32198~a;
  $$block32198~a: local33286 := null; goto block32215;
  block32215: local33303 := t; goto $$block32215~j;
  $$block32215~j: stack0o := local33303; goto $$block32215~i;
  $$block32215~i: havoc stack1s; goto $$block32215~h;
  $$block32215~h: assume $IsTokenForType(stack1s, C); goto $$block32215~g;
  $$block32215~g: stack1o := TypeObject(C); goto $$block32215~f;
  $$block32215~f: assert (stack0o != null); goto $$block32215~e;
  $$block32215~e: assert ((((($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame])) || ($Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame]))) && ($Heap[stack0o, $inv] == C)) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block32215~d;
  $$block32215~d: $Heap := $Heap[stack0o, $inv := System.Object]; goto $$block32215~c;
  $$block32215~c: havoc temp5; goto $$block32215~b;
  $$block32215~b: $Heap := $Heap[stack0o, $exposeVersion := temp5]; goto $$block32215~a;
  $$block32215~a: assume IsHeap($Heap); goto block32232;
  block32232: assert $Is(t, CS); goto $$block32232~f;
  $$block32232~f: stack0o := t; goto $$block32232~e;
  $$block32232~e: stack1i := 1; goto $$block32232~d;
  $$block32232~d: assert (stack0o != null); goto $$block32232~c;
  $$block32232~c: assert (!($Heap[stack0o, $inv] <: CS) || ($Heap[stack0o, $localinv] == C)); goto $$block32232~b;
  $$block32232~b: $Heap := $Heap[stack0o, CS.f := stack1i]; goto $$block32232~a;
  $$block32232~a: assume IsHeap($Heap); goto block32759;
  block32759: stack0o := local33303; goto $$block32759~h;
  $$block32759~h: havoc stack1s; goto $$block32759~g;
  $$block32759~g: assume $IsTokenForType(stack1s, C); goto $$block32759~f;
  $$block32759~f: stack1o := TypeObject(C); goto $$block32759~e;
  $$block32759~e: assert (stack0o != null); goto $$block32759~d;
  $$block32759~d: assert (($Heap[stack0o, $inv] == System.Object) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block32759~c;
  $$block32759~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == stack0o)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block32759~b;
  $$block32759~b: $Heap := $Heap[stack0o, $inv := C]; goto $$block32759~a;
  $$block32759~a: assume IsHeap($Heap); goto block32283;
  block32283: goto block32300;
  block32300: goto block32776;
  block32776: stack0o := null; goto true32776to32878, false32776to32793;
  true32776to32878: assume (local33286 == stack0o); goto block32878;
  false32776to32793: assume (local33286 != stack0o); goto block32793;
  block32878: goto block32895;
  block32793: goto true32793to32878, false32793to32810;
  true32793to32878: assume ($As(local33286, Microsoft.Contracts.ICheckedException) != null); goto block32878;
  false32793to32810: assume ($As(local33286, Microsoft.Contracts.ICheckedException) == null); goto block32810;
  block32810: goto block32827;
  block32895: assert (temp3 != null); goto $$block32895~e;
  $$block32895~e: assert (($Heap[temp3, $inv] == C) && ($Heap[temp3, $localinv] == $typeof(temp3))); goto $$block32895~d;
  $$block32895~d: assert ($Heap[temp3, CS.f] != 0); goto $$block32895~c;
  $$block32895~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp3)) && ($Heap[$p, $ownerFrame] == CS)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block32895~b;
  $$block32895~b: $Heap := $Heap[temp3, $inv := CS]; goto $$block32895~a;
  $$block32895~a: assume IsHeap($Heap); goto block32827;
  block32827: goto block32844;
  block32844: goto block32861;
  block32861: goto block32419;
  block32419: goto block32436;
  block32436: goto block32453;
  block32453: return;
  
}

procedure CS..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation CS..cctor() {
  entry: goto block33813;
  block33813: goto block33932;
  block33932: goto block33949;
  block33949: goto block33966;
  block33966: return;
  
}

